src/Provers/classical.ML
changeset 51717 9e7d1c139569
parent 51703 f2e92fc0c8aa
child 51718 c18cf90cb392
     1.1 --- a/src/Provers/classical.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -45,10 +45,10 @@
     1.4    val delSWrapper: Proof.context * string -> Proof.context
     1.5    val addWrapper: Proof.context * (string * (Proof.context -> wrapper)) -> Proof.context
     1.6    val delWrapper: Proof.context * string -> Proof.context
     1.7 -  val addSbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
     1.8 -  val addSafter: Proof.context * (string * (int -> tactic)) -> Proof.context
     1.9 -  val addbefore: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.10 -  val addafter: Proof.context * (string * (int -> tactic)) -> Proof.context
    1.11 +  val addSbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.12 +  val addSafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.13 +  val addbefore: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.14 +  val addafter: Proof.context * (string * (Proof.context -> int -> tactic)) -> Proof.context
    1.15    val addD2: Proof.context * (string * thm) -> Proof.context
    1.16    val addE2: Proof.context * (string * thm) -> Proof.context
    1.17    val addSD2: Proof.context * (string * thm) -> Proof.context
    1.18 @@ -670,17 +670,21 @@
    1.19    (map_uwrappers (delete_warn ("No such unsafe wrapper in claset: " ^ name) name));
    1.20  
    1.21  (* compose a safe tactic alternatively before/after safe_step_tac *)
    1.22 -fun ctxt addSbefore (name, tac1) = ctxt addSWrapper (name, fn _ => fn tac2 => tac1 ORELSE' tac2);
    1.23 -fun ctxt addSafter (name, tac2) = ctxt addSWrapper (name, fn _ => fn tac1 => tac1 ORELSE' tac2);
    1.24 +fun ctxt addSbefore (name, tac1) =
    1.25 +  ctxt addSWrapper (name, fn ctxt => fn tac2 => tac1 ctxt ORELSE' tac2);
    1.26 +fun ctxt addSafter (name, tac2) =
    1.27 +  ctxt addSWrapper (name, fn ctxt => fn tac1 => tac1 ORELSE' tac2 ctxt);
    1.28  
    1.29  (*compose a tactic alternatively before/after the step tactic *)
    1.30 -fun ctxt addbefore (name, tac1) = ctxt addWrapper (name, fn _ => fn tac2 => tac1 APPEND' tac2);
    1.31 -fun ctxt addafter (name, tac2) = ctxt addWrapper (name, fn _ => fn tac1 => tac1 APPEND' tac2);
    1.32 +fun ctxt addbefore (name, tac1) =
    1.33 +  ctxt addWrapper (name, fn ctxt => fn tac2 => tac1 ctxt APPEND' tac2);
    1.34 +fun ctxt addafter (name, tac2) =
    1.35 +  ctxt addWrapper (name, fn ctxt => fn tac1 => tac1 APPEND' tac2 ctxt);
    1.36  
    1.37 -fun ctxt addD2 (name, thm) = ctxt addafter (name, dtac thm THEN' assume_tac);
    1.38 -fun ctxt addE2 (name, thm) = ctxt addafter (name, etac thm THEN' assume_tac);
    1.39 -fun ctxt addSD2 (name, thm) = ctxt addSafter (name, dmatch_tac [thm] THEN' eq_assume_tac);
    1.40 -fun ctxt addSE2 (name, thm) = ctxt addSafter (name, ematch_tac [thm] THEN' eq_assume_tac);
    1.41 +fun ctxt addD2 (name, thm) = ctxt addafter (name, fn _ => dtac thm THEN' assume_tac);
    1.42 +fun ctxt addE2 (name, thm) = ctxt addafter (name, fn _ => etac thm THEN' assume_tac);
    1.43 +fun ctxt addSD2 (name, thm) = ctxt addSafter (name, fn _ => dmatch_tac [thm] THEN' eq_assume_tac);
    1.44 +fun ctxt addSE2 (name, thm) = ctxt addSafter (name, fn _ => ematch_tac [thm] THEN' eq_assume_tac);
    1.45  
    1.46  
    1.47