1.1 --- a/src/Provers/classical.ML	Fri May 13 23:59:48 2011 +0200
     1.2 +++ b/src/Provers/classical.ML	Sat May 14 00:32:16 2011 +0200
     1.3 @@ -942,7 +942,9 @@
     1.4    Method.setup @{binding fast} (cla_method' fast_tac) "classical prover (depth-first)" #>
     1.5    Method.setup @{binding slow} (cla_method' slow_tac) "classical prover (slow depth-first)" #>
     1.6    Method.setup @{binding best} (cla_method' best_tac) "classical prover (best-first)" #>
     1.7 -  Method.setup @{binding deepen} (cla_method' (fn ctxt => deepen_tac ctxt 4))
     1.8 +  Method.setup @{binding deepen}
     1.9 +    (Scan.lift (Scan.optional Parse.nat 4) --| Method.sections cla_modifiers
    1.10 +      >> (fn n => fn ctxt => SIMPLE_METHOD' (deepen_tac ctxt n)))
    1.11      "classical prover (iterative deepening)" #>
    1.12    Method.setup @{binding safe} (cla_method (CHANGED_PROP o safe_tac))
    1.13      "classical prover (apply safe rules)";

     2.1 --- a/src/ZF/ex/LList.thy	Fri May 13 23:59:48 2011 +0200
     2.2 +++ b/src/ZF/ex/LList.thy	Sat May 14 00:32:16 2011 +0200
     2.3 @@ -113,8 +113,7 @@
     2.4  apply (erule llist.cases)
     2.5  apply (simp_all add: QInl_def QInr_def llist.con_defs)
     2.6  (*LCons case: I simply can't get rid of the deepen_tac*)
     2.7 -apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
     2.8 -  addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
     2.9 +apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
    2.10  done
    2.11  
    2.12  lemma llist_quniv: "llist(quniv(A)) \<subseteq> quniv(A)"
    2.13 @@ -216,8 +215,7 @@
    2.14  apply (erule llist.cases, simp_all)
    2.15  apply (simp_all add: QInl_def QInr_def llist.con_defs)
    2.16  (*LCons case: I simply can't get rid of the deepen_tac*)
    2.17 -apply (tactic "deepen_tac (@{context} addIs [@{thm Ord_trans}]
    2.18 -  addIs [@{thm Int_lower1} RS @{thm subset_trans}]) 2 1")
    2.19 +apply (deepen 2 intro: Ord_trans Int_lower1 [THEN subset_trans])
    2.20  done
    2.21  
    2.22  lemma flip_in_quniv: "l \<in> llist(bool) ==> flip(l) \<in> quniv(bool)"