src/Provers/classical.ML
changeset 24218 fbf1646b267c
parent 24021 491c68f40bc4
child 24358 d75af3e90e82
     1.1 --- a/src/Provers/classical.ML	Fri Aug 10 17:04:20 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Aug 10 17:04:24 2007 +0200
     1.3 @@ -1022,7 +1022,7 @@
     1.4  
     1.5  fun default_tac rules ctxt cs facts =
     1.6    HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
     1.7 -  ClassPackage.default_intro_classes_tac facts;
     1.8 +  Class.default_intro_classes_tac facts;
     1.9  
    1.10  in
    1.11    val rule = METHOD_CLASET' o rule_tac;