diff -r d616a0912245 -r 86c60d55373c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 15:11:49 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:24:11 2009 +0100
@@ -923,6 +923,25 @@
 
 section {* Cleaning of the Theorem *}
 
+ML {*
+fun fun_map_simple_conv xs ctxt ctrm =
+  case (term_of ctrm) of
+    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
+        if (member (op=) xs h) 
+        then Conv.all_conv ctrm
+        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
+  | _ => Conv.all_conv ctrm
+
+fun fun_map_conv xs ctxt ctrm =
+  case (term_of ctrm) of
+      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
+                fun_map_simple_conv xs ctxt) ctrm
+    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
+    | _ => Conv.all_conv ctrm
+
+fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
+*}
+
 (* Since the patterns for the lhs are different; there are 3 different make-insts *)
 (* 1: does  ? \<rightarrow> id *)
 (* 2: does id \<rightarrow> ? *)
@@ -1027,38 +1046,17 @@
 fun lambda_prs_tac ctxt = CONVERSION (lambda_prs_conv ctxt)
 *}
 
-(* 1. conversion (is not a pattern) *)
-thm lambda_prs
-(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
-(*    prservation lemma                                           *)
-(*    and simplification with                                     *)
-thm all_prs ex_prs 
+(* 1. folding of definitions and preservation lemmas;  *)
+(*    and simplification with                          *)
+thm babs_prs all_prs ex_prs 
+(* 2. unfolding of ---> in front of everything, except *)
+(*    bound variables                                  *)
+thm fun_map_simps
 (* 3. simplification with *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
+thm Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 4. Test for refl *)
 
 ML {*
-fun fun_map_simple_conv xs ctxt ctrm =
-  case (term_of ctrm) of
-    ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
-        if (member (op=) xs h) 
-        then Conv.all_conv ctrm
-        else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
-  | _ => Conv.all_conv ctrm
-
-fun fun_map_conv xs ctxt ctrm =
-  case (term_of ctrm) of
-      _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
-                fun_map_simple_conv xs ctxt) ctrm
-    | Abs _ => Conv.abs_conv (fn (x, ctxt) => fun_map_conv ((term_of x)::xs) ctxt) ctxt ctrm
-    | _ => Conv.all_conv ctrm
-
-fun fun_map_tac ctxt = CONVERSION (fun_map_conv [] ctxt)
-*}
-
-
-
-ML {*
 fun clean_tac lthy =
   let
     val thy = ProofContext.theory_of lthy;