# HG changeset patch
# User haftmann
# Date 1168366140 -3600
# Node ID a995f9a8f6697e7e1d288f1644fb9ee765141d41
# Parent  990b5077590d174a8d1307bb3b3abdcd38027950
cleanup

diff -r 990b5077590d -r a995f9a8f669 src/Pure/Tools/codegen_consts.ML
--- a/src/Pure/Tools/codegen_consts.ML	Tue Jan 09 19:08:59 2007 +0100
+++ b/src/Pure/Tools/codegen_consts.ML	Tue Jan 09 19:09:00 2007 +0100
@@ -75,14 +75,11 @@
     get_first get_def specs
   end;
 
-fun mk_classop_typinst thy (c, tyco) =
-  (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
-    (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
-
 fun norm thy (c, insts) =
   let
     fun disciplined _ [(Type (tyco, _))] =
-          mk_classop_typinst thy (c, tyco)
+          (c, [Type (tyco, map (fn v => TVar ((v, 0), []))
+            (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))])
       | disciplined sort _ =
           (c, [TVar (("'a", 0), sort)]);
     fun ad_hoc c tys =
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;