src/Cube/Example.thy
changeset 19943 26b37721b357
parent 19931 fb32b43e7f80
child 30510 4120fc59dd85
--- 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 = {*