--- a/Quot/QuotMain.thy	Sat Dec 12 16:40:29 2009 +0100
+++ b/Quot/QuotMain.thy	Sat Dec 12 18:01:22 2009 +0100
@@ -329,12 +329,12 @@
        if i = i' then rtrm 
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
-  | (rt, qt) =>
+  | _ =>
        let 
-         val rts = Syntax.string_of_term lthy rt
-         val qts = Syntax.string_of_term lthy qt
+         val rtrm_str = Syntax.string_of_term lthy rtrm
+         val qtrm_str = Syntax.string_of_term lthy qtrm
        in
-         raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))
+         raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
        end
 *}
 
@@ -375,7 +375,7 @@
   val goal = Const (@{const_name "equivp"}, dummyT) $ R2  
              |> Syntax.check_term ctxt
              |> HOLogic.mk_Trueprop 
-  val eqv_prem = Goal.prove ctxt [] [] goal (fn {context,...} => equiv_tac context 1)
+  val eqv_prem = Goal.prove ctxt [] [] goal (fn _ => equiv_tac ctxt 1)
   val thm = (@{thm eq_reflection} OF [thm OF [eqv_prem]])
   val R1c = cterm_of thy R1
   val thmi = Drule.instantiate' [] [SOME R1c] thm
@@ -609,7 +609,7 @@
   by(auto simp add: QUOT_TRUE_def)
 
 ML {*
-fun quot_true_conv1 ctxt fnctn ctrm =
+fun quot_true_simple_conv ctxt fnctn ctrm =
   case (term_of ctrm) of
     (Const (@{const_name QUOT_TRUE}, _) $ x) =>
     let
@@ -629,14 +629,15 @@
 fun quot_true_conv ctxt fnctn ctrm =
   case (term_of ctrm) of
     (Const (@{const_name QUOT_TRUE}, _) $ _) =>
-      quot_true_conv1 ctxt fnctn ctrm
+      quot_true_simple_conv ctxt fnctn ctrm
   | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
   | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
   | _ => Conv.all_conv ctrm
 *}
 
 ML {*
-fun quot_true_tac ctxt fnctn = CONVERSION
+fun quot_true_tac ctxt fnctn = 
+   CONVERSION
     ((Conv.params_conv ~1 (fn ctxt =>
        (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 *}
@@ -723,7 +724,7 @@
          in
            (rtac thm THEN' quotient_tac ctxt) i
          end
-         handle _ => no_tac) (* what is the catch for ? *)
+         handle _ => no_tac) (* what is the catch for ? Should go away, no? *)
     | _ => no_tac)
 *}
 
@@ -731,7 +732,7 @@
 fun inj_repabs_tac_match ctxt = SUBGOAL (fn (goal, i) =>
 (case (bare_concl goal) of
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
-  ((Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _))
+  (Const (@{const_name fun_rel}, _) $ _ $ _) $ (Abs _) $ (Abs _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
@@ -763,7 +764,8 @@
     (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
       => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
 
-| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => (rtac @{thm refl} ORELSE'
+| Const (@{const_name "op ="},_) $ (R $ _ $ _) $ (_ $ _ $ _) => 
+   (rtac @{thm refl} ORELSE'
     (equals_rsp_tac R ctxt THEN' RANGE [
        quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]))
 
@@ -777,9 +779,10 @@
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *)
 | _ $ _ $ _
-    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) ORELSE' rep_abs_rsp_tac ctxt
+    => (rtac @{thm quot_rel_rsp} THEN_ALL_NEW quotient_tac ctxt) 
+       ORELSE' rep_abs_rsp_tac ctxt
 
-| _ => error "inj_repabs_tac not a relation"
+| _ => K no_tac
 ) i)
 *}
 
@@ -823,7 +826,8 @@
 section {* Cleaning of the Theorem *}
 
 ML {*
-(* expands all ---> except in front of bound variables *)
+(* expands all fun_maps, 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 $ _) =>