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