# HG changeset patch
# User ballarin
# Date 1150994905 -7200
# Node ID 26b37721b357eae89853fd867f06eec3720ee62f
# Parent  dc92e3aebc71c103de5ba66cf888b5a84e2d493e
Removed debugging code.

diff -r dc92e3aebc71 -r 26b37721b357 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Thu Jun 22 07:08:04 2006 +0200
+++ b/src/Cube/Example.thy	Thu Jun 22 18:48:25 2006 +0200
@@ -16,7 +16,7 @@
 
 method_setup depth_solve = {*
   Method.thms_args (fn thms => Method.METHOD (fn facts =>
-  (DEPTH_SOLVE (HEADGOAL (ares_tac (PolyML.print (facts @ thms)))))))
+  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms))))))
 *} ""
 
 method_setup depth_solve1 = {*