1.1 --- a/src/Pure/Isar/method.ML	Wed Nov 29 15:44:58 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Nov 29 15:44:59 2006 +0100
     1.3 @@ -29,7 +29,8 @@
     1.4    val insert: thm list -> method
     1.5    val insert_facts: method
     1.6    val SIMPLE_METHOD: tactic -> method
     1.7 -  val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
     1.8 +  val SIMPLE_METHOD': (int -> tactic) -> method
     1.9 +  val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
    1.10    val defer: int option -> method
    1.11    val prefer: int -> method
    1.12    val cheating: bool -> Proof.context -> method
    1.13 @@ -163,7 +164,8 @@
    1.14  fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
    1.15  
    1.16  fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
    1.17 -fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
    1.18 +fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
    1.19 +val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
    1.20  
    1.21  end;
    1.22  
    1.23 @@ -182,8 +184,8 @@
    1.24  
    1.25  (* unfold intro/elim rules *)
    1.26  
    1.27 -fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
    1.28 -fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
    1.29 +fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
    1.30 +fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
    1.31  
    1.32  
    1.33  (* unfold/fold definitions *)
    1.34 @@ -194,7 +196,7 @@
    1.35  
    1.36  (* atomize rule statements *)
    1.37  
    1.38 -fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
    1.39 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
    1.40    | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
    1.41  
    1.42  
    1.43 @@ -205,8 +207,8 @@
    1.44  
    1.45  (* fact -- composition by facts from context *)
    1.46  
    1.47 -fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt)
    1.48 -  | fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules);
    1.49 +fun fact [] ctxt = SIMPLE_METHOD' (ProofContext.some_fact_tac ctxt)
    1.50 +  | fact rules _ = SIMPLE_METHOD' (ProofContext.fact_tac rules);
    1.51  
    1.52  
    1.53  (* assumption *)
    1.54 @@ -538,13 +540,13 @@
    1.55    (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
    1.56  
    1.57  fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
    1.58 -  (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
    1.59 +  (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
    1.60  
    1.61  fun goal_args args tac = goal_args' (Scan.lift args) tac;
    1.62  
    1.63  fun goal_args_ctxt' args tac src ctxt =
    1.64    #2 (syntax (Args.goal_spec HEADGOAL -- args >>
    1.65 -  (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
    1.66 +  (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
    1.67  
    1.68  fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;
    1.69