author | ballarin |
Tue, 09 Dec 2008 13:11:42 +0100 | |
changeset 29029 | 1945e0185097 |
parent 29028 | b5dad96c755a |
child 29030 | 0ea94f540548 |
--- a/src/Pure/Isar/class.ML Tue Dec 09 11:30:24 2008 +0100 +++ b/src/Pure/Isar/class.ML Tue Dec 09 13:11:42 2008 +0100 @@ -394,7 +394,8 @@ end; fun default_intro_tac ctxt [] = - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [] + intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE + Locale.intro_locales_tac true ctxt [] | default_intro_tac _ _ = no_tac; fun default_tac rules ctxt facts =