# HG changeset patch
# User bulwahn
# Date 1329238750 -3600
# Node ID 837f79bdd3c4a20294fc14a302c3eff6296fb4ff
# Parent  cf1bcfb34c82d2d10b71492e434bca5cc00f92a9
removing debug code in mutabelle

diff -r cf1bcfb34c82 -r 837f79bdd3c4 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Tue Feb 14 17:58:51 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Tue Feb 14 17:59:10 2012 +0100
@@ -43,14 +43,6 @@
  end;
 
 
-(*possibility to print a given term for debugging purposes*)
-
-fun prt x = Pretty.writeln (Syntax.pretty_term_global @{theory Main} x);
-
-val debug = (Unsynchronized.ref false);
-fun debug_msg mutterm = if (!debug) then (prt mutterm) else ();
-
-
 (*thrown in case the specified path doesn't exist in the specified term*)
 
 exception WrongPath of string;