# HG changeset patch
# User haftmann
# Date 1161333893 -7200
# Node ID ce6759d1d0b4e25a766be5a0c656de01d320773e
# Parent  42669b5bf98edb5225ee56f9de2034cbb57c0b50
code nofunc now permits theorems violating typing discipline

diff -r 42669b5bf98e -r ce6759d1d0b4 src/Pure/Tools/codegen_data.ML
--- 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