
diff -r 2d9de77d5687 -r d616a0912245 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 06:21:09 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:11:49 2009 +0100
@@ -1038,32 +1038,39 @@
 (* 4. Test for refl *)
 
 ML {*
-fun fun_map_conv xs ctxt ctrm =
+fun fun_map_simple_conv xs ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
-        (Conv.binop_conv (fun_map_conv xs ctxt) then_conv
-        (if (member (op=) xs h) 
-         then Conv.all_conv 
-         else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]})) ctrm
-    | _ $ _ => Conv.comb_conv (fun_map_conv xs ctxt) ctrm
+        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;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
       (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
+    
     val thms1 = defs @ (prs_rules_get lthy) @ @{thms babs_prs all_prs ex_prs}
-    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy)
+    val thms2 = @{thms Quotient_abs_rep Quotient_rel_rep} @ (id_simps_get lthy) 
     fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
   in
     EVERY' [simp_tac (simps thms1),
-            TRY o REPEAT_ALL_NEW (CHANGED o (fun_map_tac lthy)),
+            fun_map_tac lthy,
             lambda_prs_tac lthy,
             simp_tac (simps thms2),
             TRY o rtac refl]




