code nofunc now permits theorems violating typing discipline

--- a/src/Pure/Tools/codegen_data.ML	Fri Oct 20 10:44:51 2006 +0200
+++ b/src/Pure/Tools/codegen_data.ML	Fri Oct 20 10:44:53 2006 +0200
@@ -75,7 +75,7 @@
   | NONE => ["[...]"];
 
 fun pretty_lthms ctxt r = case Susp.peek r
- of SOME thms => (map (ProofContext.pretty_thm ctxt) o rev) thms
+ of SOME thms => map (ProofContext.pretty_thm ctxt) thms
   | NONE => [Pretty.str "[...]"];
 
 fun certificate thy f r =
@@ -642,7 +642,7 @@
 
 fun del_func thm thy =
   let
-    val thms = mk_func thy thm;
+    val thms = setmp strict_functyp false (mk_func thy) thm;
     val cs = map fst thms;
   in
     map_exec_purge (SOME cs) (map_funcs