# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260416108 -3600
# Node ID cf1ad0e59d970e88c56647d64bbeb2e2142e9954
# Parent  2ff666f644ccf95772942004a3a3c0d695fdf8c3
completed previous commit

diff -r 2ff666f644cc -r cf1ad0e59d97 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 04:34:24 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 04:35:08 2009 +0100
@@ -212,19 +212,6 @@
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
 
-section {* Debugging infrastructure for testing tactics *}
-
-ML {*
-fun my_print_tac ctxt s i thm =
-let
-  val prem_str = nth (prems_of thm) (i - 1)
-                 |> Syntax.string_of_term ctxt
-                 handle Subscript => "no subgoal"
-  val _ = tracing (s ^ "\n" ^ prem_str)
-in
-  Seq.single thm
-end *}
-
 section {* Matching of Terms and Types *}
 
 ML {*