# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259922889 -3600
# Node ID fdfeef0399f748a0c3d741bd00670f2777486f90
# Parent  cc1f240d8cf468578407af877abac9e3c59701aa# Parent  ebfd747b47ab07605d1881ae19348e4bd1222e0d
merged

diff -r ebfd747b47ab -r fdfeef0399f7 QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 11:34:49 2009 +0100
@@ -795,7 +795,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