# HG changeset patch # User wenzelm # Date 1201215078 -3600 # Node ID 2cfb703fa8d8eade3bceaf16f72d6625b5d53ee6 # Parent dae57244f1c7f32e8e6a034c76121c01a292b246 improved apply: handle thread position, apply to context here; replaced ContextPosition by Position.thread_position; diff -r dae57244f1c7 -r 2cfb703fa8d8 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Jan 24 23:51:17 2008 +0100 +++ b/src/Pure/Isar/method.ML Thu Jan 24 23:51:18 2008 +0100 @@ -17,7 +17,7 @@ signature METHOD = sig include BASIC_METHOD - val apply: method -> thm list -> cases_tactic + val apply: Position.T -> (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 @@ -133,7 +133,8 @@ datatype method = Meth of thm list -> cases_tactic; -fun apply (Meth m) = m; +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) (); val RAW_METHOD_CASES = Meth; @@ -219,14 +220,15 @@ if cond (Logic.strip_assums_concl prop) then Tactic.rtac rule i else no_tac); -fun legacy_tac ctxt st = - (legacy_feature ("implicit use of prems in assumption proof" ^ ContextPosition.str_of ctxt); +fun legacy_tac st = + (legacy_feature + ("implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ())); all_tac st); fun assm_tac ctxt = assume_tac APPEND' Goal.assume_rule_tac ctxt APPEND' - (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K (legacy_tac ctxt)) APPEND' + (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K legacy_tac) APPEND' cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND' cond_rtac (can Logic.dest_term) Drule.termI;