src/HOL/Tools/specification_package.ML
changeset 22709 9ab51bac6287
parent 22578 b0eb5652f210
child 22902 ac833b4bb7ee
     1.1 --- a/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:49 2007 +0200
     1.2 +++ b/src/HOL/Tools/specification_package.ML	Sun Apr 15 23:25:50 2007 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4          val thawed_prop_consts = collect_consts (prop_thawed,[])
     1.5          val (altcos,overloaded) = Library.split_list cos
     1.6          val (names,sconsts) = Library.split_list altcos
     1.7 -        val consts = map (term_of o Thm.read_cterm thy o rpair TypeInfer.logicT) sconsts
     1.8 +        val consts = map (term_of o Thm.read_cterm thy o rpair dummyT) sconsts
     1.9          val _ = not (Library.exists (not o Term.is_Const) consts)
    1.10            orelse error "Specification: Non-constant found as parameter"
    1.11