diff --git a/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry b/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry
deleted file mode 100644
index 00e8e557..00000000
--- a/Primitive/Symmetric/Cipher/Block/AES_parameterized.cry
+++ /dev/null
@@ -1,43 +0,0 @@
-/*
-   Copyright (c) 2018 Galois, Inc.
-   www.cryptol.net
-*/
-
-module Primitive::Symmetric::Cipher::Block::AES_parameterized where
-
-import `Primitive::Symmetric::Cipher::Block::AES::Algorithm as AES
-import `Primitive::Symmetric::Cipher::Block::AES::ExpandKey
-import Primitive::Symmetric::Cipher::Block::AES::TBox
-
-type constraint ValidKey k m = (k == 128 + m * 64, 2 >= m)
-
-type EncKey m = AES::KeySchedule m
-type DecKey m = AES::KeySchedule m
-
-
-encrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
-encrypt k = encryptWithSchedule (expandKeyEnc k)
-
-decrypt : {k,m} ValidKey k m => [k] -> [128] -> [128]
-decrypt k = decryptWithSchedule (expandKeyDec k)
-
-
-expandKeyEnc : {k,m} ValidKey k m => [k] -> EncKey m
-expandKeyEnc = expandKey`{Nk = AES::Nk m, Nr = AES::Nr m}
-
-encryptWithSchedule : {k,m} ValidKey k m => EncKey m -> [128] -> [128]
-encryptWithSchedule = AES::encrypt params
-
-
-
-expandKeyDec : {k,m} ValidKey k m => [k] -> EncKey m
-expandKeyDec k = makeDecKey (expandKey`{Nk = AES::Nk m, Nr = AES::Nr m} k)
-
-decryptWithSchedule : {k,m} ValidKey k m => DecKey m -> [128] -> [128]
-decryptWithSchedule = AES::decrypt params
-
-
-params = { encRound = AESRound, decRound = AESInvRound }
-
-property test k pt = decrypt k (encrypt k pt) == pt
-