diff -r 990b5077590d -r a995f9a8f669 src/Pure/Tools/codegen_func.ML
--- a/src/Pure/Tools/codegen_func.ML	Tue Jan 09 19:08:59 2007 +0100
+++ b/src/Pure/Tools/codegen_func.ML	Tue Jan 09 19:09:00 2007 +0100
@@ -116,28 +116,6 @@
 val check_func = gen_check_func true;
 val legacy_check_func = gen_check_func false;
 
-fun check_typ_classop thm =
-  let
-    val thy = Thm.theory_of_thm thm;
-    val (c_ty as (c, ty), _) = dest_func thm;
-  in case AxClass.class_of_param thy c
-   of SOME class => let
-        val const = CodegenConsts.norm_of_typ thy c_ty;
-        val ty_decl = CodegenConsts.disc_typ_of_const thy
-            (snd o CodegenConsts.typ_of_inst thy) const;
-        val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy);
-      in if Sign.typ_equiv thy (ty_decl, ty)
-        then thm
-        else error
-          ("Type\n" ^ string_of_typ ty
-           ^ "\nof function theorem\n"
-           ^ string_of_thm thm
-           ^ "\nis strictly less general than declared function type\n"
-           ^ string_of_typ ty_decl)
-      end
-    | NONE => thm
-  end;
-
 fun gen_mk_func check_func = map_filter check_func o mk_rew;
 val mk_func = gen_mk_func check_func;
 val legacy_mk_func = gen_mk_func legacy_check_func;