improved apply: handle thread position, apply to context here;
authorwenzelm
Thu Jan 24 23:51:18 2008 +0100 (2008-01-24)
changeset 259572cfb703fa8d8
parent 25956 dae57244f1c7
child 25958 bcedde463850
improved apply: handle thread position, apply to context here;
replaced ContextPosition by Position.thread_position;
src/Pure/Isar/method.ML
     1.1 --- a/src/Pure/Isar/method.ML	Thu Jan 24 23:51:17 2008 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Thu Jan 24 23:51:18 2008 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  signature METHOD =
     1.5  sig
     1.6    include BASIC_METHOD
     1.7 -  val apply: method -> thm list -> cases_tactic
     1.8 +  val apply: Position.T -> (Proof.context -> method) -> Proof.context -> thm list -> cases_tactic
     1.9    val RAW_METHOD_CASES: (thm list -> cases_tactic) -> method
    1.10    val RAW_METHOD: (thm list -> tactic) -> method
    1.11    val METHOD_CASES: (thm list -> cases_tactic) -> method
    1.12 @@ -133,7 +133,8 @@
    1.13  
    1.14  datatype method = Meth of thm list -> cases_tactic;
    1.15  
    1.16 -fun apply (Meth m) = m;
    1.17 +fun apply pos meth_fun ctxt facts goal = Position.setmp_thread_data_seq pos
    1.18 +  (fn () => let val Meth meth = meth_fun ctxt in meth facts goal end) ();
    1.19  
    1.20  val RAW_METHOD_CASES = Meth;
    1.21  
    1.22 @@ -219,14 +220,15 @@
    1.23    if cond (Logic.strip_assums_concl prop)
    1.24    then Tactic.rtac rule i else no_tac);
    1.25  
    1.26 -fun legacy_tac ctxt st =
    1.27 -  (legacy_feature ("implicit use of prems in assumption proof" ^ ContextPosition.str_of ctxt);
    1.28 +fun legacy_tac st =
    1.29 +  (legacy_feature
    1.30 +      ("implicit use of prems in assumption proof" ^ Position.str_of (Position.thread_data ()));
    1.31      all_tac st);
    1.32  
    1.33  fun assm_tac ctxt =
    1.34    assume_tac APPEND'
    1.35    Goal.assume_rule_tac ctxt APPEND'
    1.36 -  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K (legacy_tac ctxt)) APPEND'
    1.37 +  (CHANGED o solve_tac (Assumption.prems_of ctxt) THEN' K legacy_tac) APPEND'
    1.38    cond_rtac (can Logic.dest_equals) Drule.reflexive_thm APPEND'
    1.39    cond_rtac (can Logic.dest_term) Drule.termI;
    1.40