NewLocale.intro_locales_tac added to Class.default_intro_tac.
1.1 --- a/src/Pure/Isar/class.ML Tue Dec 09 11:30:24 2008 +0100
1.2 +++ b/src/Pure/Isar/class.ML Tue Dec 09 13:11:42 2008 +0100
1.3 @@ -394,7 +394,8 @@
1.4 end;
1.5
1.6 fun default_intro_tac ctxt [] =
1.7 - intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
1.8 + intro_classes_tac [] ORELSE NewLocale.intro_locales_tac true ctxt [] ORELSE
1.9 + Locale.intro_locales_tac true ctxt []
1.10 | default_intro_tac _ _ = no_tac;
1.11
1.12 fun default_tac rules ctxt facts =