--- a/QuotMain.thy	Fri Dec 04 21:43:29 2009 +0100
+++ b/QuotMain.thy	Sat Dec 05 00:06:27 2009 +0100
@@ -283,16 +283,6 @@
   end
 *}
 
-ML {*
-fun lookup_quot_consts defs =
-  let
-    fun dest_term (a $ b) = (a, b);
-    val def_terms = map (snd o Logic.dest_equals o concl_of) defs;
-  in
-    map (fst o dest_Const o snd o dest_term) def_terms
-  end
-*}
-
 section {* Regularization *} 
 
 (*
@@ -937,21 +927,26 @@
 *}
 
 ML {*
+val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
+*}
+
+ML {*
 fun rep_abs_rsp_tac ctxt =
   SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of (rel $ _ $ (rep $ (abs $ _))) =>
-    (let
-      val thy = ProofContext.theory_of ctxt;
-      val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
-      val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
-      val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
-      val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
-      val te = solve_quotient_assums ctxt thm
-    in
-      rtac te i
-    end
-    handle _ => no_tac)
-  | _ => no_tac)
+    case (bare_concl goal) of 
+      (rel $ _ $ (rep $ (abs $ _))) =>
+        (let
+           val thy = ProofContext.theory_of ctxt;
+           val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+           val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+           val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+           val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+           val te = solve_quotient_assums ctxt thm
+         in
+           rtac te i
+         end
+         handle _ => no_tac)
+    | _ => no_tac)
 *}
 
 lemma fun_rel_id:
@@ -962,7 +957,7 @@
 
 ML {*
 fun inj_repabs_tac_match ctxt trans2 = SUBGOAL (fn (goal, i) =>
-(case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
+(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 _))
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam