# HG changeset patch
# User wenzelm
# Date 1460903807 -7200
# Node ID 56cf1249ee203e1984d86f76740df51418dcd801
# Parent  637ed69b4d46c19a633e4d7a70aa35476a86da71
removed pointless check (see Type_Infer.object_logic);

diff -r 637ed69b4d46 -r 56cf1249ee20 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 16:28:35 2016 +0200
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Apr 17 16:36:47 2016 +0200
@@ -151,7 +151,7 @@
     (fname, qs, gs, args, rhs)
   end
 
-(*check for all sorts of errors in the input*)
+(*check for various errors in the input*)
 fun check_defs ctxt fixes eqs =
   let
     val fnames = map (fst o fst) fixes
@@ -203,17 +203,7 @@
     val _ = null not_defined
       orelse error ("No defining equations for function" ^
         plural " " "s " not_defined ^ commas_quote not_defined)
-
-    fun check_sorts ((fname, fT), _) =
-      Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
-      orelse error (cat_lines
-      ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
-       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
-
-    val _ = map check_sorts fixes
-  in
-    ()
-  end
+  in () end
 
 
 (* preprocessors *)