unfold_locales now part of default tactic

--- a/src/Provers/classical.ML	Fri Mar 28 22:01:04 2008 +0100
+++ b/src/Provers/classical.ML	Fri Mar 28 22:01:56 2008 +0100
@@ -1019,7 +1019,7 @@
 
 fun default_tac rules ctxt cs facts =
   HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
-  Class.default_intro_classes_tac facts;
+  Class.default_intro_tac ctxt facts;
 
 in
   val rule = METHOD_CLASET' o rule_tac;

--- a/src/Pure/Isar/class.ML	Fri Mar 28 22:01:04 2008 +0100
+++ b/src/Pure/Isar/class.ML	Fri Mar 28 22:01:56 2008 +0100
@@ -21,7 +21,7 @@
   val refresh_syntax: class -> Proof.context -> Proof.context
 
   val intro_classes_tac: thm list -> tactic
-  val default_intro_classes_tac: thm list -> tactic
+  val default_intro_tac: Proof.context -> thm list -> tactic
   val prove_subclass: class * class -> thm -> theory -> theory
 
   val class_prefix: string -> string
@@ -388,12 +388,13 @@
     Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
   end;
 
-fun default_intro_classes_tac [] = intro_classes_tac []
-  | default_intro_classes_tac _ = no_tac;
+fun default_intro_tac ctxt [] =
+      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+  | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =
   HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
-    default_intro_classes_tac facts;
+    default_intro_tac ctxt facts;
 
 val _ = Context.>> (Context.map_theory
   (Method.add_methods