src/Pure/Isar/method.ML
changeset 18939 18e2a2676d80
parent 18921 f47c46d7d654
child 18999 e0eb9cb97db0
     1.1 --- a/src/Pure/Isar/method.ML	Mon Feb 06 20:59:05 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Feb 06 20:59:06 2006 +0100
     1.3 @@ -176,7 +176,7 @@
     1.4  (* shuffle subgoals *)
     1.5  
     1.6  fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
     1.7 -fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
     1.8 +fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
     1.9  
    1.10  
    1.11  (* cheating *)
    1.12 @@ -333,7 +333,7 @@
    1.13  in
    1.14  
    1.15  fun iprover_tac ctxt opt_lim =
    1.16 -  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1);
    1.17 +  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    1.18  
    1.19  end;
    1.20