# HG changeset patch
# User ballarin
# Date 1228824702 -3600
# Node ID 1945e01850972607555f276aefc45a8d88f10f93
# Parent  b5dad96c755a15e9ca20fe6570bd3dfed405995c
NewLocale.intro_locales_tac added to Class.default_intro_tac.

diff -r b5dad96c755a -r 1945e0185097 src/Pure/Isar/class.ML
--- 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 =