src/Provers/classical.ML
changeset 35613 9d3ff36ad4e1
parent 33522 737589bb9bb8
child 35625 9c818cab0dd0
     1.1 --- a/src/Provers/classical.ML	Sat Mar 06 15:34:29 2010 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Mar 06 15:39:16 2010 +0100
     1.3 @@ -125,8 +125,8 @@
     1.4    val haz_intro: int option -> attribute
     1.5    val rule_del: attribute
     1.6    val cla_modifiers: Method.modifier parser list
     1.7 -  val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
     1.8 -  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
     1.9 +  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
    1.10 +  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
    1.11    val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.12    val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
    1.13    val setup: theory -> theory
    1.14 @@ -969,14 +969,14 @@
    1.15    Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
    1.16    Args.del -- Args.colon >> K (I, rule_del)];
    1.17  
    1.18 -fun cla_meth tac prems ctxt = METHOD (fn facts =>
    1.19 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
    1.20 +fun cla_meth tac ctxt = METHOD (fn facts =>
    1.21 +  ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
    1.22  
    1.23 -fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    1.24 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
    1.25 +fun cla_meth' tac ctxt = METHOD (fn facts =>
    1.26 +  HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
    1.27  
    1.28 -fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    1.29 -fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    1.30 +fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
    1.31 +fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);
    1.32  
    1.33  
    1.34