--- a/QuotMain.thy	Fri Dec 04 11:06:43 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:34:21 2009 +0100
@@ -805,7 +805,7 @@
               val [R2, f, g, x, y] = map (cterm_of thy) [R2, f, g, x, y];
               val t_inst = [NONE, NONE, NONE, SOME R2, NONE, NONE, SOME f, SOME g, SOME x, SOME y];
               val thm = Drule.instantiate' ty_inst t_inst @{thm APPLY_RSP}
-              (*val _ = tracing (Syntax.string_of_term @{context} (prop_of thm))*)
+              val _ = tracing ("instantiated rule" ^ Syntax.string_of_term @{context} (prop_of thm))
             in
               rtac thm 1
             end