src/HOL/Tools/specification_package.ML
changeset 21116 be58cded79da
parent 20903 905effde63d9
child 21359 072e83a0b5bb
--- a/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:01 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML	Tue Oct 31 09:29:06 2006 +0100
@@ -140,7 +140,7 @@
         val prop  = myfoldr HOLogic.mk_conj (map fst props'')
         val cprop = cterm_of thy (HOLogic.mk_Trueprop prop)
 
-        val (prop_thawed,vmap) = Type.varify (prop,[])
+        val (vmap, prop_thawed) = Type.varify [] prop
         val thawed_prop_consts = collect_consts (prop_thawed,[])
         val (altcos,overloaded) = Library.split_list cos
         val (names,sconsts) = Library.split_list altcos
@@ -150,7 +150,7 @@
 
         fun proc_const c =
             let
-                val c' = fst (Type.varify (c,[]))
+                val (_, c') = Type.varify [] c
                 val (cname,ctyp) = dest_Const c'
             in
                 case List.filter (fn t => let val (name,typ) = dest_Const t