src/HOL/Tools/choice_specification.ML
changeset 56254 a2dd9200854d
parent 54742 7a86358a3c0b
child 56270 ce9c7a527c4b
     1.1 --- a/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/choice_specification.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4          fun proc_single prop =
     1.5              let
     1.6                  val frees = Misc_Legacy.term_frees prop
     1.7 -                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
     1.8 +                val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
     1.9                    orelse error "Specificaton: Only free variables of sort 'type' allowed"
    1.10                  val prop_closed = close_form prop
    1.11              in