--- 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;
--- 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 =
--- 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
--- 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