src/Pure/Isar/method.ML
changeset 27235 134991516430
parent 26892 9454a8bd1114
child 27244 af0a44372d1f
     1.1 --- a/src/Pure/Isar/method.ML	Mon Jun 16 17:54:48 2008 +0200
     1.2 +++ b/src/Pure/Isar/method.ML	Mon Jun 16 17:54:49 2008 +0200
     1.3 @@ -51,8 +51,9 @@
     1.4    val drule: int -> thm list -> method
     1.5    val frule: int -> thm list -> method
     1.6    val iprover_tac: Proof.context -> int option -> int -> tactic
     1.7 -  val set_tactic: (Proof.context -> thm list -> tactic) -> Proof.context -> Proof.context
     1.8 +  val set_tactic: (thm list -> tactic) -> Proof.context -> Proof.context
     1.9    val tactic: string * Position.T -> Proof.context -> method
    1.10 +  val raw_tactic: string * Position.T -> Proof.context -> method
    1.11    type src
    1.12    datatype text =
    1.13      Basic of (Proof.context -> method) * Position.T |
    1.14 @@ -355,7 +356,7 @@
    1.15  
    1.16  structure TacticData = ProofDataFun
    1.17  (
    1.18 -  type T = Proof.context -> thm list -> tactic;
    1.19 +  type T = thm list -> tactic;
    1.20    fun init _ = undefined;
    1.21  );
    1.22  
    1.23 @@ -364,10 +365,10 @@
    1.24  fun ml_tactic (txt, pos) ctxt =
    1.25    let
    1.26      val ctxt' = ctxt |> Context.proof_map
    1.27 -      (ML_Context.expression Position.none
    1.28 -        "fun tactic (ctxt: Proof.context) (facts: thm list) : tactic"
    1.29 +      (ML_Context.expression pos
    1.30 +        "fun tactic (facts: thm list) : tactic"
    1.31          "Context.map_proof (Method.set_tactic tactic)" txt);
    1.32 -  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt' ctxt) end;
    1.33 +  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
    1.34  
    1.35  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
    1.36  fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);