# HG changeset patch
# User haftmann
# Date 1168003910 -3600
# Node ID 6466a24dee5b283aa6d647e9f6c25cb4dcf23814
# Parent  e52aef4ab54b14fd4f4b3f704dc47b7a81cd029e
some cleanup

diff -r e52aef4ab54b -r 6466a24dee5b src/Pure/Tools/codegen_funcgr.ML
--- a/src/Pure/Tools/codegen_funcgr.ML	Fri Jan 05 14:31:49 2007 +0100
+++ b/src/Pure/Tools/codegen_funcgr.ML	Fri Jan 05 14:31:50 2007 +0100
@@ -16,7 +16,6 @@
   val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list
   val all: T -> CodegenConsts.const list
   val norm_varnames: theory -> thm list -> thm list
-  val expand_eta: theory -> int -> thm -> thm
   val print_codethms: theory -> CodegenConsts.const list -> unit
   structure Constgraph : GRAPH
 end;
@@ -51,42 +50,13 @@
 
 (** theorem purification **)
 
-fun expand_eta thy k thm =
-  let
-    val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm;
-    val (head, args) = strip_comb lhs;
-    val l = Int.max (0, k - length args);
-    val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
-    fun get_name _ 0 used = ([], used)
-      | get_name (Abs (v, ty, t)) k used =
-          used
-          |> Name.variants [CodegenNames.purify_var v]
-          ||>> get_name t (k - 1)
-          |>> (fn ([v'], vs') => (v', ty) :: vs')
-      | get_name t k used = 
-          let
-            val (tys, _) = (strip_type o fastype_of) t
-          in case tys
-           of [] => raise TERM ("expand_eta", [t])
-            | ty :: _ =>
-                used
-                |> Name.variants [""]
-                |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
-                #>> (fn vs' => (v, ty) :: vs'))
-          end;
-    val (vs, _) = get_name rhs l used;
-    val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
-  in
-    fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
-  end;
-
 fun norm_args thy thms =
   let
     val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
     val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0;
   in
     thms
-    |> map (expand_eta thy k)
+    |> map (CodegenFunc.expand_eta thy k)
     |> map (Drule.fconv_rule Drule.beta_eta_conversion)
   end;
 
diff -r e52aef4ab54b -r 6466a24dee5b src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Fri Jan 05 14:31:49 2007 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Fri Jan 05 14:31:50 2007 +0100
@@ -93,7 +93,7 @@
     val ty = (Logic.unvarifyT o CodegenData.typ_func thy) thm;
     val thms' = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
       then thms
-      else map (CodegenFuncgr.expand_eta thy 1) thms;
+      else map (CodegenFunc.expand_eta thy 1) thms;
   in (ty, thms') end;