--- a/src/Provers/classical.ML Sat Mar 06 15:34:29 2010 +0100
+++ b/src/Provers/classical.ML Sat Mar 06 15:39:16 2010 +0100
@@ -125,8 +125,8 @@
val haz_intro: int option -> attribute
val rule_del: attribute
val cla_modifiers: Method.modifier parser list
- val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
- val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+ val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
+ val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
val cla_method: (claset -> tactic) -> (Proof.context -> Proof.method) context_parser
val cla_method': (claset -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
val setup: theory -> theory
@@ -969,14 +969,14 @@
Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
Args.del -- Args.colon >> K (I, rule_del)];
-fun cla_meth tac prems ctxt = METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
+fun cla_meth tac ctxt = METHOD (fn facts =>
+ ALLGOALS (Method.insert_tac facts) THEN tac (claset_of ctxt));
-fun cla_meth' tac prems ctxt = METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
+fun cla_meth' tac ctxt = METHOD (fn facts =>
+ HEADGOAL (Method.insert_tac facts THEN' tac (claset_of ctxt)));
-fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
-fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
+fun cla_method tac = Method.sections cla_modifiers >> K (cla_meth tac);
+fun cla_method' tac = Method.sections cla_modifiers >> K (cla_meth' tac);