# HG changeset patch
# User haftmann
# Date 1162303166 -3600
# Node ID 8e621232a865a5b66db9513c5696bc9dc8f31869
# Parent  7b2624686fc34f858c40f9c27a74e85daa5dddb2
clarified make_term interface

diff -r 7b2624686fc3 -r 8e621232a865 src/Pure/Tools/codegen_funcgr.ML
--- 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*)
 
diff -r 7b2624686fc3 -r 8e621232a865 src/Pure/Tools/codegen_package.ML
--- 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;
 
diff -r 7b2624686fc3 -r 8e621232a865 src/Pure/Tools/nbe.ML
--- 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