src/Provers/classical.ML
changeset 14605 9de4d64eee3b
parent 13525 cafd1f98d658
child 15036 cab1c1fc1851
     1.1 --- a/src/Provers/classical.ML	Fri Apr 16 20:34:41 2004 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Apr 16 20:59:09 2004 +0200
     1.3 @@ -924,7 +924,8 @@
     1.4  
     1.5  (** proof methods **)
     1.6  
     1.7 -(* METHOD_CLASET' *)
     1.8 +fun METHOD_CLASET tac ctxt =
     1.9 +  Method.METHOD (tac ctxt (get_local_claset ctxt));
    1.10  
    1.11  fun METHOD_CLASET' tac ctxt =
    1.12    Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
    1.13 @@ -947,12 +948,12 @@
    1.14    | rule_tac rules _ _ facts = Method.rule_tac rules facts;
    1.15  
    1.16  fun default_tac rules ctxt cs facts =
    1.17 -  rule_tac rules ctxt cs facts ORELSE'
    1.18 +  HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
    1.19    AxClass.default_intro_classes_tac facts;
    1.20  
    1.21  in
    1.22    val rule = METHOD_CLASET' o rule_tac;
    1.23 -  val default = METHOD_CLASET' o default_tac;
    1.24 +  val default = METHOD_CLASET o default_tac;
    1.25  end;
    1.26  
    1.27