Graceful treatment of non-locale subgoals by methods unfold_locales and intro_locales.

--- a/NEWS	Mon Feb 15 01:27:06 2010 +0100
+++ b/NEWS	Mon Feb 15 01:34:08 2010 +0100
@@ -9,6 +9,8 @@
 * Code generator: details of internal data cache have no impact on
 the user space functionality any longer.
 
+* Methods unfold_locales and intro_locales ignore non-locale subgoals.  This
+is more appropriate for interpretations with 'where'.  INCOMPATIBILITY.
 
 *** HOL ***
 

--- a/src/Pure/Isar/locale.ML	Mon Feb 15 01:27:06 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Mon Feb 15 01:34:08 2010 +0100
@@ -566,15 +566,22 @@
 
 
 (* Tactic *)
+fun intros_tac intros facts =
+  (TRYALL (Method.insert_tac facts THEN'
+      REPEAT_ALL_NEW (resolve_tac intros)) |> CHANGED)
+    THEN Tactic.distinct_subgoals_tac;
 
-fun intro_locales_tac eager ctxt =
-  Method.intros_tac
+fun gen_intro_locales_tac intros_tac eager ctxt =
+  intros_tac
     (get_witnesses ctxt @ get_intros ctxt @ (if eager then get_unfolds ctxt else []));
 
+val intro_locales_tac = gen_intro_locales_tac Method.intros_tac;
+val try_intro_locales_tac= gen_intro_locales_tac Method.try_intros_tac;
+
 val _ = Context.>> (Context.map_theory
- (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o intro_locales_tac false))
+ (Method.setup (Binding.name "intro_locales") (Scan.succeed (METHOD o try_intro_locales_tac false))
     "back-chain introduction rules of locales without unfolding predicates" #>
-  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o intro_locales_tac true))
+  Method.setup (Binding.name "unfold_locales") (Scan.succeed (METHOD o try_intro_locales_tac true))
     "back-chain all introduction rules of locales"));
 
 end;

--- a/src/Pure/Isar/method.ML	Mon Feb 15 01:27:06 2010 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 15 01:34:08 2010 +0100
@@ -46,6 +46,7 @@
   val rule_tac: thm list -> thm list -> int -> tactic
   val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic
   val intros_tac: thm list -> thm list -> tactic
+  val try_intros_tac: thm list -> thm list -> tactic
   val rule: thm list -> method
   val erule: int -> thm list -> method
   val drule: int -> thm list -> method
@@ -262,11 +263,13 @@
 
 (* intros_tac -- pervasive search spanned by intro rules *)
 
-fun intros_tac intros facts =
-  ALLGOALS (insert_tac facts THEN'
+fun gen_intros_tac goals intros facts =
+  goals (insert_tac facts THEN'
       REPEAT_ALL_NEW (resolve_tac intros))
     THEN Tactic.distinct_subgoals_tac;
 
+val intros_tac = gen_intros_tac ALLGOALS;
+val try_intros_tac = gen_intros_tac TRYALL;
 
 (* ML tactics *)