diff -r f48b8a82c1e3 -r 4335435fcf83 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sat Dec 12 15:23:58 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 16:40:29 2009 +0100
@@ -823,6 +823,7 @@
 section {* Cleaning of the Theorem *}
 
 ML {*
+(* expands all ---> except in front of bound variables *)
 fun fun_map_simple_conv xs ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
@@ -844,34 +845,30 @@
 (* Since the patterns for the lhs are different; there are 2 different make-insts *)
 (* 1: does  ? \<rightarrow> id *)
 (* 2: does  ? \<rightarrow> non-id *)
-ML {*
+ML {* 
+fun mk_abs u i t =
+  if incr_boundvars i u aconv t then Bound i
+  else (case t of
+     t1 $ t2 => (mk_abs u i t1) $ (mk_abs u i t2)
+   | Abs (s, T, t') => Abs (s, T, mk_abs u (i + 1) t')
+   | Bound j => if i = j then error "make_inst" else t
+   | _ => t)
+
 fun make_inst lhs t =
-  let
-    val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
-    val _ $ (Abs (_, _, g)) = t;
-    fun mk_abs i t =
-      if incr_boundvars i u aconv t then Bound i
-      else (case t of
-        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
-      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
-      | Bound j => if i = j then error "make_inst" else t
-      | _ => t);
-  in (f, Abs ("x", T, mk_abs 0 g)) end;
-*}
+let
+  val _ $ (Abs (_, _, (f as Var (_, Type ("fun", [T, _]))) $ u)) = lhs;
+  val _ $ (Abs (_, _, g)) = t;
+in 
+  (f, Abs ("x", T, mk_abs u 0 g)) 
+end
 
-ML {*
 fun make_inst2 lhs t =
-  let
-    val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
-    val _ $ (Abs (_, _, (_ $ g))) = t;
-    fun mk_abs i t =
-      if incr_boundvars i u aconv t then Bound i
-      else (case t of
-        t1 $ t2 => mk_abs i t1 $ mk_abs i t2
-      | Abs (s, T, t') => Abs (s, T, mk_abs (i + 1) t')
-      | Bound j => if i = j then error "make_inst" else t
-      | _ => t);
-  in (f, Abs ("x", T, mk_abs 0 g)) end;
+let
+  val _ $ (Abs (_, _, (_ $ ((f as Var (_, Type ("fun", [T, _]))) $ u)))) = lhs;
+  val _ $ (Abs (_, _, (_ $ g))) = t;
+in 
+  (f, Abs ("x", T, mk_abs u 0 g)) 
+end
 *}
 
 ML {*
@@ -1005,8 +1002,8 @@
 (* the QUOT_TRUE premise in 2 records the lifted theorem *)
 
 ML {*
-  val lifting_procedure = 
-    @{lemma  "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)}
+val lifting_procedure = 
+   @{lemma  "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)}
 *}
 
 ML {*