src/HOL/Tools/choice_specification.ML

           map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
 
         fun proc_single prop =
             let
                 val frees = Misc_Legacy.term_frees prop
-                val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+                val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
                   orelse error "Specificaton: Only free variables of sort 'type' allowed"
                 val prop_closed = close_form prop
             in
                 (prop_closed,frees)
             end