src/Pure/Isar/method.ML
changeset 58957 c9e744ea8a38
parent 58950 d07464875dd4
child 58963 26bf09b95dda
     1.1 --- a/src/Pure/Isar/method.ML	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4    val SIMPLE_METHOD': (int -> tactic) -> method
     1.5    val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
     1.6    val cheating: Proof.context -> bool -> method
     1.7 -  val intro: thm list -> method
     1.8 -  val elim: thm list -> method
     1.9 +  val intro: Proof.context -> thm list -> method
    1.10 +  val elim: Proof.context -> thm list -> method
    1.11    val unfold: thm list -> Proof.context -> method
    1.12    val fold: thm list -> Proof.context -> method
    1.13    val atomize: bool -> Proof.context -> method
    1.14 @@ -127,8 +127,8 @@
    1.15  
    1.16  (* unfold intro/elim rules *)
    1.17  
    1.18 -fun intro ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ths));
    1.19 -fun elim ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ths));
    1.20 +fun intro ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (match_tac ctxt ths));
    1.21 +fun elim ctxt ths = SIMPLE_METHOD' (CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac ctxt ths));
    1.22  
    1.23  
    1.24  (* unfold/fold definitions *)
    1.25 @@ -590,9 +590,9 @@
    1.26      "do nothing (insert current facts only)" #>
    1.27    setup @{binding insert} (Attrib.thms >> (K o insert))
    1.28      "insert theorems, ignoring facts (improper)" #>
    1.29 -  setup @{binding intro} (Attrib.thms >> (K o intro))
    1.30 +  setup @{binding intro} (Attrib.thms >> (fn ths => fn ctxt => intro ctxt ths))
    1.31      "repeatedly apply introduction rules" #>
    1.32 -  setup @{binding elim} (Attrib.thms >> (K o elim))
    1.33 +  setup @{binding elim} (Attrib.thms >> (fn ths => fn ctxt => elim ctxt ths))
    1.34      "repeatedly apply elimination rules" #>
    1.35    setup @{binding unfold} (Attrib.thms >> unfold_meth) "unfold definitions" #>
    1.36    setup @{binding fold} (Attrib.thms >> fold_meth) "fold definitions" #>