# HG changeset patch
# User wenzelm
# Date 1164811499 -3600
# Node ID 8831206d7f419480209cb8597faa76e50953fbbc
# Parent  5e0f2340caa7cca2113016f844af75b2a3800404
renamed SIMPLE_METHOD' to SIMPLE_METHOD'';
added simple version of SIMPLE_METHOD';

diff -r 5e0f2340caa7 -r 8831206d7f41 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Nov 29 15:44:58 2006 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 29 15:44:59 2006 +0100
@@ -29,7 +29,8 @@
   val insert: thm list -> method
   val insert_facts: method
   val SIMPLE_METHOD: tactic -> method
-  val SIMPLE_METHOD': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
+  val SIMPLE_METHOD': (int -> tactic) -> method
+  val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
   val defer: int option -> method
   val prefer: int -> method
   val cheating: bool -> Proof.context -> method
@@ -163,7 +164,8 @@
 fun insert thms = METHOD (fn _ => ALLGOALS (insert_tac thms));
 
 fun SIMPLE_METHOD tac = METHOD (fn facts => ALLGOALS (insert_tac facts) THEN tac);
-fun SIMPLE_METHOD' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
+fun SIMPLE_METHOD'' quant tac = METHOD (fn facts => quant (insert_tac facts THEN' tac));
+val SIMPLE_METHOD' = SIMPLE_METHOD'' HEADGOAL;
 
 end;
 
@@ -182,8 +184,8 @@
 
 (* unfold intro/elim rules *)
 
-fun intro ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
-fun elim ths = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
+fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.match_tac ths));
+fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (Tactic.ematch_tac ths));
 
 
 (* unfold/fold definitions *)
@@ -194,7 +196,7 @@
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' HEADGOAL (CHANGED_PROP o ObjectLogic.atomize_tac)
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_tac)
   | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
 
 
@@ -205,8 +207,8 @@
 
 (* fact -- composition by facts from context *)
 
-fun fact [] ctxt = SIMPLE_METHOD' HEADGOAL (ProofContext.some_fact_tac ctxt)
-  | fact rules _ = SIMPLE_METHOD' HEADGOAL (ProofContext.fact_tac rules);
+fun fact [] ctxt = SIMPLE_METHOD' (ProofContext.some_fact_tac ctxt)
+  | fact rules _ = SIMPLE_METHOD' (ProofContext.fact_tac rules);
 
 
 (* assumption *)
@@ -538,13 +540,13 @@
   (#2 oo syntax (Scan.lift (Scan.optional (Args.parens Args.nat) 0) -- Attrib.thms));
 
 fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >>
-  (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt);
+  (fn (quant, s) => SIMPLE_METHOD'' quant (tac s))) src ctxt);
 
 fun goal_args args tac = goal_args' (Scan.lift args) tac;
 
 fun goal_args_ctxt' args tac src ctxt =
   #2 (syntax (Args.goal_spec HEADGOAL -- args >>
-  (fn (quant, s) => SIMPLE_METHOD' quant (tac ctxt s))) src ctxt);
+  (fn (quant, s) => SIMPLE_METHOD'' quant (tac ctxt s))) src ctxt);
 
 fun goal_args_ctxt args tac = goal_args_ctxt' (Scan.lift args) tac;