--- a/Quot/QuotMain.thy	Tue Dec 08 01:25:43 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 04:14:02 2009 +0100
@@ -144,6 +144,7 @@
 
 declare [[map * = (prod_fun, prod_rel)]]
 declare [[map "fun" = (fun_map, fun_rel)]]
+
 (* Throws now an exception:              *)
 (* declare [[map "option" = (bla, blu)]] *)
 
@@ -253,7 +254,7 @@
 fun NDT ctxt s tac thm = tac thm  
 *}
 
-section {* Matching of terms and types *}
+section {* Matching of Terms and Types *}
 
 ML {*
 fun matches_typ (ty, ty') =
@@ -266,9 +267,7 @@
        then (List.all matches_typ (tys ~~ tys')) 
        else false
   | _ => false
-*}
 
-ML {*
 fun matches_term (trm, trm') = 
    case (trm, trm') of 
      (_, Var _) => true
@@ -453,9 +452,7 @@
 fun equiv_tac ctxt =
   (K (print_tac "equiv tac")) THEN'
   REPEAT_ALL_NEW (resolve_tac (equiv_rules_get ctxt))
-*}
 
-ML {*
 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss)
 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac
 *}
@@ -497,7 +494,7 @@
   SOME thm2
 end
 handle _ => NONE
-(* FIXME/TODO: what is the place where the exception can be raised: matching_prs? *)
+(* FIXME/TODO: what is the place where the exception is raised: matching_prs? *)
 *}
 
 ML {*
@@ -616,8 +613,7 @@
         val yvar = Free (y, T)
         val result = Term.lambda_name (y, yvar) (inj_repabs_trm lthy (s, s'))
       in
-        if rty = qty 
-        then result
+        if rty = qty then result
         else mk_repabs lthy (rty, qty) result
       end
 
@@ -625,8 +621,7 @@
        (inj_repabs_trm lthy (t, t')) $ (inj_repabs_trm lthy (s, s'))
 
   | (Free (_, T), Free (_, T')) => 
-        if T = T' 
-        then rtrm 
+        if T = T' then rtrm 
         else mk_repabs lthy (T, T') rtrm
 
   | (_, Const (@{const_name "op ="}, _)) => rtrm
@@ -636,8 +631,7 @@
       let
         val rty = fastype_of rtrm
       in 
-        if rty = T'                    
-        then rtrm
+        if rty = T' then rtrm
         else mk_repabs lthy (rty, T') rtrm
       end   
   
@@ -651,10 +645,7 @@
   REPEAT_ALL_NEW (FIRST'
     [rtac @{thm identity_quotient},
      resolve_tac (quotient_rules_get ctxt)])
-*}
 
-(* solver for the simplifier *)
-ML {*
 fun quotient_solver_tac ss = quotient_tac (Simplifier.the_context ss)
 val quotient_solver = Simplifier.mk_solver' "Quotient goal solver" quotient_solver_tac
 *}
@@ -940,15 +931,12 @@
 in
   inj_repabs_step_tac ctxt rel_refl trans2
 end
-*}
 
-ML {*
 fun all_inj_repabs_tac ctxt =
   REPEAT_ALL_NEW (inj_repabs_tac ctxt)
-(* if this is too slow we can inline the code above *)
 *}
 
-section {* Cleaning of the theorem *}
+section {* Cleaning of the Theorem *}
 
 ML {*
 fun make_inst lhs t =
@@ -1034,8 +1022,8 @@
 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
 (*    and simplification with                                     *)
 thm all_prs ex_prs 
-(* 3. simplification with id_simps and *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep
+(* 3. simplification with *)
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps
 (* 4. Test for refl *)
 
 ML {*
@@ -1043,7 +1031,7 @@
   let
     val thy = ProofContext.theory_of lthy;
     val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
-      (* FIXME: shouldn't the definitions already be varified? *)
+      (* FIXME: why is the Thm.varifyT needed: example where it fails is LamEx *)
     val thms1 = @{thms all_prs ex_prs} @ defs
     val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
                 @ @{thms Quotient_abs_rep Quotient_rel_rep} 
@@ -1155,12 +1143,22 @@
 *}
 
 ML {*
-(* automated tactics *)
+fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+
+fun WARN (tac, msg) i st =
+ case Seq.pull ((SOLVES' tac) i st) of
+     NONE    => (warning msg; Seq.single st)
+   | seqcell => Seq.make (fn () => seqcell)
+
+fun RANGE_WARN xs = RANGE (map WARN xs)
+*}
+
+ML {*
 fun lift_tac ctxt rthm =
   procedure_tac ctxt rthm
-  THEN' RANGE [regularize_tac ctxt,
-               all_inj_repabs_tac ctxt,
-               clean_tac ctxt]
+  THEN' RANGE_WARN [(regularize_tac ctxt,     "Regularize proof failed."),
+                    (all_inj_repabs_tac ctxt, "Injection proof failed."),
+                    (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
 end