# HG changeset patch
# User wenzelm
# Date 1248537855 -7200
# Node ID 966e166d039d97bb80dd3ee5c3bbe7db45ce97f6
# Parent  c314b48360310dab42504052b6348cf649d3e563
Method.Basic: no position;

diff -r c314b4836031 -r 966e166d039d src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Sat Jul 25 18:02:43 2009 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Sat Jul 25 18:04:15 2009 +0200
@@ -380,7 +380,7 @@
       [goals] |>
     Proof.apply (Method.Basic (fn _ => RAW_METHOD (fn _ =>
       rewrite_goals_tac defs_thms THEN
-      compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
+      compose_tac (false, rule, length rule_prems) 1)) |>
     Seq.hd
   end;
 
diff -r c314b4836031 -r 966e166d039d src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sat Jul 25 18:02:43 2009 +0200
+++ b/src/HOL/Statespace/state_space.ML	Sat Jul 25 18:04:15 2009 +0200
@@ -149,7 +149,7 @@
    thy
    |> Expression.sublocale_cmd name expr
    |> Proof.global_terminal_proof
-         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt),Position.none), NONE)
+         (Method.Basic (fn ctxt => SIMPLE_METHOD (ctxt_tac ctxt)), NONE)
    |> ProofContext.theory_of
 
 fun add_locale name expr elems thy =
diff -r c314b4836031 -r 966e166d039d src/HOL/Tools/Function/fundef_datatype.ML
--- a/src/HOL/Tools/Function/fundef_datatype.ML	Sat Jul 25 18:02:43 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_datatype.ML	Sat Jul 25 18:04:15 2009 +0200
@@ -208,13 +208,12 @@
 
 val by_pat_completeness_auto =
     Proof.global_future_terminal_proof
-      (Method.Basic (pat_completeness, Position.none),
+      (Method.Basic pat_completeness,
        SOME (Method.Source_i (Args.src (("HOL.auto", []), Position.none))))
 
 fun termination_by method int =
     Fundef.termination_proof NONE
-    #> Proof.global_future_terminal_proof
-      (Method.Basic (method, Position.none), NONE) int
+    #> Proof.global_future_terminal_proof (Method.Basic method, NONE) int
 
 fun mk_catchall fixes arity_of =
     let
diff -r c314b4836031 -r 966e166d039d src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sat Jul 25 18:02:43 2009 +0200
+++ b/src/Pure/Isar/element.ML	Sat Jul 25 18:04:15 2009 +0200
@@ -272,7 +272,7 @@
   Proof.refine (Method.Basic (K (RAW_METHOD
     (K (ALLGOALS
       (CONJUNCTS (ALLGOALS
-        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
+        (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
 
 fun gen_witness_proof proof after_qed wit_propss eq_props =
   let