--- a/QuotMain.thy	Mon Nov 30 11:53:20 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 12:14:20 2009 +0100
@@ -947,7 +947,7 @@
 
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)