# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259922861 -3600
# Node ID cc1f240d8cf468578407af877abac9e3c59701aa
# Parent  14f68c1f4d12e691d347cf4ebce0274f864384d9
merged

diff -r 14f68c1f4d12 -r cc1f240d8cf4 QuotMain.thy
--- 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