--- 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 {*