--- a/src/Pure/Tools/codegen_funcgr.ML Tue Oct 31 14:58:23 2006 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML Tue Oct 31 14:59:26 2006 +0100
@@ -10,7 +10,7 @@
sig
type T;
val make: theory -> CodegenConsts.const list -> T
- val make_term: theory -> cterm -> (cterm * (thm * (thm -> thm))) * T
+ val make_term: theory -> ((thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T
val funcs: T -> CodegenConsts.const -> thm list
val typ: T -> CodegenConsts.const -> typ
val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
@@ -337,7 +337,7 @@
fun make thy consts =
Funcgr.change thy (ensure_consts thy consts);
-fun make_term thy ct =
+fun make_term thy f ct =
let
val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct);
val _ = Term.fold_types (Type.no_tvars #> K I) (Thm.term_of ct) ();
@@ -373,7 +373,7 @@
(* val _ = writeln "ADD INST"; *)
val funcgr' = ensure_consts thy
(instdefs_of thy (fold (fold (insert (op =)) o insts_of thy funcgr) cs [])) funcgr
- in ((ct'', (thm5, drop)), Funcgr.change thy (K funcgr')) end;
+ in (f drop ct'' thm5, Funcgr.change thy (K funcgr')) end;
end; (*local*)
--- a/src/Pure/Tools/codegen_package.ML Tue Oct 31 14:58:23 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Oct 31 14:59:26 2006 +0100
@@ -588,7 +588,7 @@
fun codegen_term thy t =
let
val ct = Thm.cterm_of thy t;
- val ((ct', _), funcgr) = CodegenFuncgr.make_term thy ct;
+ val (ct', funcgr) = CodegenFuncgr.make_term thy (K K) ct;
val t' = Thm.term_of ct';
in generate thy funcgr (SOME []) NONE exprgen_term' t' end;
--- a/src/Pure/Tools/nbe.ML Tue Oct 31 14:58:23 2006 +0100
+++ b/src/Pure/Tools/nbe.ML Tue Oct 31 14:59:26 2006 +0100
@@ -188,15 +188,18 @@
fun normalization_conv ct =
let
val thy = Thm.theory_of_cterm ct;
- val ((ct', (thm1, drop_classes)), _) = CodegenFuncgr.make_term thy ct;
- val t = Thm.term_of ct';
- val thm2 = normalization_invoke thy t;
- val thm3 = apply_posts thy ((snd o Drule.dest_equals o Thm.cprop_of) thm2);
- in
- Thm.transitive thm1 (drop_classes (Thm.transitive thm2 thm3)) handle
- THM _ => error ("normalization_conv - could not construct proof:\n"
- ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
- end;
+ fun mk drop_classes ct thm1 =
+ let
+ val t = Thm.term_of ct;
+ val thm2 = normalization_invoke thy t;
+ val thm3 = apply_posts thy ((snd o Drule.dest_equals o Thm.cprop_of) thm2);
+ val thm23 = drop_classes (Thm.transitive thm2 thm3);
+ in
+ Thm.transitive thm1 thm23 handle THM _ =>
+ error ("normalization_conv - could not construct proof:\n"
+ ^ (cat_lines o map string_of_thm) [thm1, thm2, thm3])
+ end;
+ in fst (CodegenFuncgr.make_term thy mk ct) end;
fun norm_print_term ctxt modes t =
let