proper collapse_let

--- a/src/Pure/Tools/codegen_package.ML	Thu Jun 28 19:09:38 2007 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Thu Jun 28 19:09:41 2007 +0200
@@ -2,7 +2,7 @@
     ID:         $Id$
     Author:     Florian Haftmann, TU Muenchen
 
-Code generator extraction kernel. Code generator Isar setup.
+Code generator translation kernel.  Code generator Isar setup.
 *)
 
 signature CODEGEN_PACKAGE =
@@ -12,12 +12,13 @@
   val satisfies: theory -> term -> string list -> bool;
   val codegen_command: theory -> string -> unit;
 
+  (*axiomatic interfaces*)
   type appgen;
   val add_appconst: string * appgen -> theory -> theory;
+  val appgen_let: appgen;
   val appgen_case: (theory -> term
     -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
     -> appgen;
-  val appgen_let: appgen;
 
   val timing: bool ref;
 end;
@@ -30,7 +31,7 @@
 val succeed = CodegenThingol.succeed;
 val fail = CodegenThingol.fail;
 
-(** code extraction **)
+(** code translation **)
 
 (* theory data *)
 
@@ -119,7 +120,7 @@
   in (ty, thms') end;
 
 
-(* extraction kernel *)
+(* translation kernel *)
 
 fun check_strict (false, _) has_seri x =
       false
@@ -394,7 +395,7 @@
         |> appgen_default thy algbr funcgr strct ((c, ty), ts);
 
 
-(* entrance points into extraction kernel *)
+(* entrance points into translation kernel *)
 
 fun ensure_def_const' thy algbr funcgr strct c trns =
   ensure_def_const thy algbr funcgr strct c trns
@@ -419,7 +420,7 @@
 
 
 (* parametrized application generators, for instantiation in object logic *)
-(* (axiomatic extensions of extraction kernel *)
+(* (axiomatic extensions of translation kernel) *)
 
 fun appgen_case dest_case_expr thy algbr funcgr strct (app as (c_ty, ts)) trns =
   let
@@ -440,11 +441,7 @@
   trns
   |> exprgen_term thy algbr funcgr strct ct
   ||>> exprgen_term thy algbr funcgr strct st
-  |-> (fn ((v, ty) `|-> be, se) =>
-            pair (ICase ((se, ty), case be
-              of ICase ((IVar w, _), ds) => if v = w then ds else [(IVar v, be)]
-               | _ => [(IVar v, be)]
-            ))
+  |-> (fn ((v, ty) `|-> be, se) => pair (CodegenThingol.collapse_let (((v, ty), se), be))
         | _ => appgen_default thy algbr funcgr strct app);
 
 fun add_appconst (c, appgen) thy =

--- a/src/Pure/Tools/codegen_thingol.ML	Thu Jun 28 19:09:38 2007 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML	Thu Jun 28 19:09:41 2007 +0200
@@ -50,6 +50,7 @@
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   val unfold_const_app: iterm ->
     ((string * (dict list list * itype list)) * iterm list) option;
+  val collapse_let: ((vname * itype) * iterm) * iterm -> iterm;
   val eta_expand: (string * (dict list list * itype list)) * iterm list -> int -> iterm;
   val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a;
@@ -224,6 +225,18 @@
           add vs td #> fold (fn (p, t) => add vs p #> add vs t) bs;
   in add [] end;
 
+fun collapse_let (((v, ty), se), be as ICase ((IVar w, _), ds)) =
+      let
+        fun exists_v t = fold_unbound_varnames (fn w => fn b =>
+          b orelse v = w) t false;
+      in if v = w andalso forall (fn (t1, t2) =>
+        exists_v t1 orelse not (exists_v t2)) ds
+        then ICase ((se, ty), ds)
+        else ICase ((se, ty), [(IVar v, be)])
+      end
+  | collapse_let (((v, ty), se), be) =
+      ICase ((se, ty), [(IVar v, be)])
+
 fun eta_expand (c as (_, (_, tys)), ts) k =
   let
     val j = length ts;