# HG changeset patch
# User haftmann
# Date 1206738116 -3600
# Node ID e44d24620515c13d22230254f3a86d3c7651bc95
# Parent  6deb216d726f8d84d20850c4e34c4c8d191082d3
unfold_locales now part of default tactic

diff -r 6deb216d726f -r e44d24620515 src/Provers/classical.ML
--- 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;
diff -r 6deb216d726f -r e44d24620515 src/Pure/Isar/class.ML
--- 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