diff -r 6793659d38d6 -r 672b94510e7d QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 11:28:19 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 11:33:24 2009 +0100
@@ -754,15 +754,6 @@
 *}
 
 ML {*
-val weak_lambda_rsp_tac =
-  SUBGOAL (fn (goal, i) =>
-    case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
-       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
-     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i
-     | _ => no_tac)
-*}
-
-ML {*
 val ball_rsp_tac = 
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
@@ -918,10 +909,9 @@
 *}
 
 ML {*
-fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) =>
-  CONVERSION
-    (Conv.params_conv ~1 (fn ctxt =>
-       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i)
+fun quot_true_tac ctxt fnctn = CONVERSION
+    ((Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn)))) ctxt)
 *}
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
@@ -933,61 +923,6 @@
     (Abs a) => snd (Term.dest_abs a)
   | _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))  *}
 
-ML {*
-fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
-  (FIRST' [
-    (* "cong" rule of the of the relation / transitivity*)
-    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    NDT ctxt "1" (resolve_tac trans2),
-
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    NDT ctxt "2" (lambda_rsp_tac),
-
-    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm ball_rsp}),
-
-    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
-    NDT ctxt "4" (ball_rsp_tac),
-
-    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "5" (rtac @{thm bex_rsp}),
-
-    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
-    NDT ctxt "6" (bex_rsp_tac),
-
-    (* respectfulness of constants *)
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
-
-    (* reflexivity of operators arising from Cong_tac *)
-    NDT ctxt "8" (rtac @{thm refl}),
-
-    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
-    (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
-                  THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
-
-    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
-                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms)]))),
-
-    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
-    (* merge with previous tactic *)
-    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
-
-    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "C" (rtac @{thm ext}),
-    
-    (* reflexivity of the basic relations *)
-    (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl),
-
-    (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac),
-
-    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
-    (* global simplification *)
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
-*}
 
 ML {*
 fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =