src/Provers/classical.ML
changeset 42798 02c88bdabe75
parent 42793 88bee9f6eec7
child 42799 4e33894aec6d
--- a/src/Provers/classical.ML	Fri May 13 23:59:48 2011 +0200
+++ b/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
@@ -942,7 +942,9 @@
   Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
   Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
   Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
-  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
+  Method.setup @{binding deepen}
+    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
+      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
     "classical prover (iterative deepening)" #>
   Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
     "classical prover (apply safe rules)";