src/Provers/classical.ML
changeset 30510 4120fc59dd85
parent 30190 479806475f3c
child 30513 1796b8ea88aa
     1.1 --- a/src/Provers/classical.ML	Fri Mar 13 19:53:09 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Fri Mar 13 19:58:26 2009 +0100
     1.3 @@ -971,11 +971,8 @@
     1.4  
     1.5  (** proof methods **)
     1.6  
     1.7 -fun METHOD_CLASET tac ctxt =
     1.8 -  Method.METHOD (tac ctxt (local_claset_of ctxt));
     1.9 -
    1.10 -fun METHOD_CLASET' tac ctxt =
    1.11 -  Method.METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
    1.12 +fun METHOD_CLASET tac ctxt = METHOD (tac ctxt (local_claset_of ctxt));
    1.13 +fun METHOD_CLASET' tac ctxt = METHOD (HEADGOAL o tac ctxt (local_claset_of ctxt));
    1.14  
    1.15  
    1.16  local
    1.17 @@ -1021,10 +1018,10 @@
    1.18    Args.$$$ introN -- Args.colon >> K (I, haz_intro NONE),
    1.19    Args.del -- Args.colon >> K (I, rule_del)];
    1.20  
    1.21 -fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
    1.22 +fun cla_meth tac prems ctxt = METHOD (fn facts =>
    1.23    ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
    1.24  
    1.25 -fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
    1.26 +fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    1.27    HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
    1.28  
    1.29  val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;