--- a/QuotMain.thy	Tue Dec 01 18:48:52 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 18:51:14 2009 +0100
@@ -5,8 +5,6 @@
      ("quotient_def.ML")
 begin
 
-thm LAMBDA_PRS
-
 ML {*
 let
    val parser = Args.context -- Scan.lift Args.name_source
@@ -811,8 +809,8 @@
 val weak_lambda_res_tac =
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
-       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} 1
-     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} 1
+       (_ $ _ $ (Abs _)) => rtac @{thm FUN_REL_I} i
+     | (_ $ (Abs _) $ _) => rtac @{thm FUN_REL_I} i
      | _ => no_tac)
 *}
 
@@ -821,7 +819,7 @@
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
         (_ $ (Const (@{const_name Ball}, _) $ _) 
-           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} 1
+           $ (Const (@{const_name Ball}, _) $ _)) => rtac @{thm FUN_REL_I} i
       |_ => no_tac)
 *}
 
@@ -830,7 +828,7 @@
   SUBGOAL (fn (goal, i) =>
     case HOLogic.dest_Trueprop (Logic.strip_imp_concl goal) of
         (_ $ (Const (@{const_name Bex}, _) $ _) 
-           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} 1
+           $ (Const (@{const_name Bex}, _) $ _)) => rtac @{thm FUN_REL_I} i
       | _ => no_tac)
 *}
 
@@ -940,19 +938,19 @@
     DT 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_res_tac ctxt),
+    NDT ctxt "2" (lambda_res_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 ctxt),
+    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 ctxt),
+    NDT ctxt "6" (bex_rsp_tac),
 
     (* respectfulness of constants *)
     NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),