src/Pure/Isar/method.ML

 
 signature METHOD =
 sig
   include BASIC_METHOD
   type method
-  val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
+  val apply: (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
   val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
   val RAW_METHOD: (thm list -> tactic) -> method
   val METHOD_CASES: (thm list -> cases_tactic) -> method
   val METHOD: (thm list -> tactic) -> method
   val fail: method

   val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
   val tactic: string * Position.T -> Proof.context -> method
   val raw_tactic: string * Position.T -> Proof.context -> method
   type src = Args.src
   datatype text =
-    Basic of (Proof.context -> method) * Position.T |
+    Basic of Proof.context -> method |
     Source of src |
     Source_i of src |
     Then of text list |
     Orelse of text list |
     Try of text |

   val succeed_text: text
   val default_text: text
   val this_text: text
   val done_text: text
   val sorry_text: bool -> text
-  val finish_text: text option * bool -> Position.T -> text
+  val finish_text: text option * bool -> text
   val print_methods: theory -> unit
   val intern: theory -> xstring -> string
   val defined: theory -> string -> bool
   val method: theory -> src -> Proof.context -> method
   val method_i: theory -> src -> Proof.context -> method

 
 (* datatype method *)
 
 datatype method = Meth of thm list -> cases_tactic;
 
-fun apply pos meth_fun ctxt facts goal = Position.setmp_thread_data_seq pos
-  (fn () => let val Meth meth = meth_fun ctxt in meth facts goal end) ();
+fun apply meth ctxt = let val Meth m = meth ctxt in m end;
 
 val RAW_METHOD_CASES = Meth;
 
 fun RAW_METHOD tac = RAW_METHOD_CASES (NO_CASES o tac);
 

 (* method text *)
 
 type src = Args.src;
 
 datatype text =
-  Basic of (Proof.context -> method) * Position.T |
+  Basic of Proof.context -> method |
   Source of src |
   Source_i of src |
   Then of text list |
   Orelse of text list |
   Try of text |
   Repeat1 of text |
   SelectGoals of int * text;
 
-fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)), Position.none);
-val succeed_text = Basic (K succeed, Position.none);
+fun primitive_text r = Basic (K (SIMPLE_METHOD (PRIMITIVE r)));
+val succeed_text = Basic (K succeed);
 val default_text = Source (Args.src (("default", []), Position.none));
-val this_text = Basic (K this, Position.none);
-val done_text = Basic (K (SIMPLE_METHOD all_tac), Position.none);
-fun sorry_text int = Basic (cheating int, Position.none);
-
-fun finish_text (NONE, immed) pos = Basic (close immed, pos)
-  | finish_text (SOME txt, immed) pos = Then [txt, Basic (close immed, pos)];
+val this_text = Basic (K this);
+val done_text = Basic (K (SIMPLE_METHOD all_tac));
+fun sorry_text int = Basic (cheating int);
+
+fun finish_text (NONE, immed) = Basic (close immed)
+  | finish_text (SOME txt, immed) = Then [txt, Basic (close immed)];
 
 
 (* method definitions *)
 
 structure Methods = TheoryDataFun

 val unfold = unfold_meth;
 val fold = fold_meth;
 
 end;
 
-structure BasicMethod: BASIC_METHOD = Method;
-open BasicMethod;
+structure Basic_Method: BASIC_METHOD = Method;
+open Basic_Method;
 
 val RAW_METHOD_CASES = Method.RAW_METHOD_CASES;
 val RAW_METHOD = Method.RAW_METHOD;
 val METHOD_CASES = Method.METHOD_CASES;
 val METHOD = Method.METHOD;