Method.Basic: include position;

--- a/src/HOL/Nominal/nominal_primrec.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -372,9 +372,9 @@
            |> Theory.parent_path
          end))
       [goals] |>
-    Proof.apply (Method.Basic (fn ctxt => Method.RAW_METHOD (fn ths =>
+    Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
       rewrite_goals_tac (map snd defs_thms') THEN
-      compose_tac (false, rule, length rule_prems) 1))) |>
+      compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
     Seq.hd
   end;
 

--- a/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -14,7 +14,7 @@
     val setup : theory -> theory
 end
 
-structure FundefDatatype (*: FUNDEF_DATATYPE*) =
+structure FundefDatatype: FUNDEF_DATATYPE =
 struct
 
 open FundefLib
@@ -199,12 +199,13 @@
 
 val by_pat_completeness_simp =
     Proof.global_terminal_proof
-      (Method.Basic (K pat_completeness),
+      (Method.Basic (K pat_completeness, Position.none),
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 val termination_by_lexicographic_order =
     FundefPackage.setup_termination_proof NONE
-    #> Proof.global_terminal_proof (Method.Basic (LexicographicOrder.lexicographic_order []), NONE)
+    #> Proof.global_terminal_proof
+      (Method.Basic (LexicographicOrder.lexicographic_order [], Position.none), NONE)
 
 fun mk_catchall fixes arities =
     let

--- a/src/Pure/Isar/element.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/Pure/Isar/element.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -306,7 +306,7 @@
   Proof.refine (Method.Basic (K (Method.RAW_METHOD
     (K (ALLGOALS
       (PRECISE_CONJUNCTS ~1 (ALLGOALS
-        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI))))))))));
+        (PRECISE_CONJUNCTS ~1 (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
 
 fun pretty_witness ctxt witn =
   let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in

--- a/src/Pure/Tools/class_package.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/Pure/Tools/class_package.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -371,13 +371,13 @@
 fun prove_interpretation tac prfx_atts expr insts thy =
   thy
   |> Locale.interpretation_i I prfx_atts expr insts
-  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
+  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   |> ProofContext.theory_of;
 
 fun prove_interpretation_in tac after_qed (name, expr) thy =
   thy
   |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
-  |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
+  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   |> ProofContext.theory_of;
 
 fun instance_sort' do_proof (class, sort) theory =

--- a/src/Pure/Tools/invoke.ML	Wed Jun 13 00:01:41 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Wed Jun 13 00:01:51 2007 +0200
@@ -93,7 +93,8 @@
       "invoke" NONE after_qed propp
     |> Element.refine_witness
     |> Seq.hd
-    |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules)))))))
+    |> Proof.refine (Method.Basic (K (Method.METHOD (K (HEADGOAL (RANGE (map rtac inst_rules))))),
+      Position.none))
     |> Seq.hd
   end;