src/Provers/classical.ML
changeset 19110 4bda27adcd2e
parent 18989 a5c3bc6fd6b6
child 19257 4463aee061bc
     1.1 --- a/src/Provers/classical.ML	Sun Feb 19 22:40:18 2006 +0100
     1.2 +++ b/src/Provers/classical.ML	Mon Feb 20 11:37:18 2006 +0100
     1.3 @@ -1029,7 +1029,7 @@
     1.4  
     1.5  fun default_tac rules ctxt cs facts =
     1.6    HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
     1.7 -  AxClass.default_intro_classes_tac facts;
     1.8 +  ClassPackage.default_intro_classes_tac facts;
     1.9  
    1.10  in
    1.11    val rule = METHOD_CLASET' o rule_tac;