--- 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