--- a/QuotMain.thy	Tue Dec 01 18:51:14 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 19:01:51 2009 +0100
@@ -905,7 +905,7 @@
 
 ML {*
 fun quot_true_tac ctxt fnctn =
-  SUBGOAL (fn (gl, _) =>
+  SUBGOAL (fn (gl, i) =>
   let
     val thy = ProofContext.theory_of ctxt;
     fun find_fun trm =
@@ -923,7 +923,7 @@
           val cty2 = ctyp_of thy (fastype_of fx);
           val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
         in
-          dtac thm 1
+          dtac thm i
         end
     | NONE => error "quot_true_tac!"
     | _ => error "quot_true_tac!!"