src/HOL/Tools/Function/function_common.ML
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 57959 1bfed12a7646
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -347,7 +347,7 @@
     1.4          plural " " "s " not_defined ^ commas_quote not_defined)
     1.5  
     1.6      fun check_sorts ((fname, fT), _) =
     1.7 -      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
     1.8 +      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
     1.9        orelse error (cat_lines
    1.10        ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
    1.11         Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])