src/HOL/Tools/specification_package.ML
changeset 20344 d02b43ea722e
parent 19876 11d447d5d68c
child 20548 8ef25fe585a8
--- a/src/HOL/Tools/specification_package.ML	Sat Aug 05 14:52:58 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sat Aug 05 14:55:09 2006 +0200
@@ -131,8 +131,7 @@
         fun proc_single prop =
             let
                 val frees = Term.term_frees prop
-                val tsig = Sign.tsig_of (sign_of thy)
-                val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
+                val _ = assert (forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees)
                                "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)
             in