diff -r 6b77cfd508e9 -r 1a4eb39ba834 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 12:20:49 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 12:21:15 2009 +0100
@@ -794,7 +794,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