let_simproc: activate Variable.import;

--- a/src/HOL/simpdata.ML	Tue Jul 11 11:19:28 2006 +0200
+++ b/src/HOL/simpdata.ML	Tue Jul 11 12:16:52 2006 +0200
@@ -176,27 +176,25 @@
 val Let_folded = thm "Let_folded";
 val Let_unfold = thm "Let_unfold";
 
-val (f_Let_unfold,x_Let_unfold) = 
-      let val [(_$(f$x)$_)] = prems_of Let_unfold 
+val (f_Let_unfold,x_Let_unfold) =
+      let val [(_$(f$x)$_)] = prems_of Let_unfold
       in (cterm_of (sign_of (the_context ())) f,cterm_of (sign_of (the_context ())) x) end
-val (f_Let_folded,x_Let_folded) = 
-      let val [(_$(f$x)$_)] = prems_of Let_folded 
+val (f_Let_folded,x_Let_folded) =
+      let val [(_$(f$x)$_)] = prems_of Let_folded
       in (cterm_of (sign_of (the_context ())) f, cterm_of (sign_of (the_context ())) x) end;
-val g_Let_folded = 
+val g_Let_folded =
       let val [(_$_$(g$_))] = prems_of Let_folded in cterm_of (sign_of (the_context ())) g end;
 in
 val let_simproc =
-  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"] 
+  Simplifier.simproc (Theory.sign_of (the_context ())) "let_simp" ["Let x f"]
    (fn sg => fn ss => fn t =>
-(* FIXME: very slow (replace t by t' in case below)
      let val ctxt = Simplifier.the_context ss;
          val ([t'],ctxt') = Variable.import_terms false [t] ctxt;
      in Option.map (hd o Variable.export ctxt' ctxt o single)
-*)
-      (case t of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
+      (case t' of (Const ("Let",_)$x$f) => (* x and f are already in normal form *)
          if not (!use_let_simproc) then NONE
-         else if is_Free x orelse is_Bound x orelse is_Const x 
-         then SOME Let_def  
+         else if is_Free x orelse is_Bound x orelse is_Const x
+         then SOME Let_def
          else
           let
              val n = case f of (Abs (x,_,_)) => x | _ => "x";
@@ -206,27 +204,25 @@
              val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
              val (_$_$g) = prop_of fx_g;
              val g' = abstract_over (x,g);
-           in (if (g aconv g') 
+           in (if (g aconv g')
                then
                   let
                     val rl = cterm_instantiate [(f_Let_unfold,cf),(x_Let_unfold,cx)] Let_unfold;
-                  in SOME (rl OF [fx_g]) end 
+                  in SOME (rl OF [fx_g]) end
                else if Term.betapply (f,x) aconv g then NONE (*avoid identity conversion*)
-               else let 
+               else let
                      val abs_g'= Abs (n,xT,g');
                      val g'x = abs_g'$x;
                      val g_g'x = symmetric (beta_conversion false (cterm_of sg g'x));
                      val rl = cterm_instantiate
                                [(f_Let_folded,cterm_of sg f),(x_Let_folded,cx),
                                 (g_Let_folded,cterm_of sg abs_g')]
-                               Let_folded; 
-                   in SOME (rl OF [transitive fx_g g_g'x]) 
+                               Let_folded;
+                   in SOME (rl OF [transitive fx_g g_g'x])
                    end)
            end
         | _ => NONE)
- (*  FIXME: continue
-  end*)
- )
+     end)
 end
 
 (*** Case splitting ***)