# HG changeset patch
# User wenzelm
# Date 1537382747 -7200
# Node ID 0c1d7a414185624048ba4f90bdd7a907c02ff1a3
# Parent  c77efde4e4fdf4144c0f4c77808b977317d44d7a
clarified signature;

diff -r c77efde4e4fd -r 0c1d7a414185 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Wed Sep 19 16:11:54 2018 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed Sep 19 20:45:47 2018 +0200
@@ -229,7 +229,7 @@
       in resolve_tac ctxt [rule] i end);
 
     fun tac ctxt =
-      Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
+      Locale.intro_locales_tac {strict = true, eager = true} ctxt [] THEN ALLGOALS (solve_tac ctxt);
 
   in
     thy |> prove_interpretation_in tac (name, parent_expr)
@@ -366,7 +366,7 @@
       let
         val expr = ([(pname, (prefix, (Expression.Positional rs,[])))],[])
       in prove_interpretation_in
-           (fn ctxt => Locale.intro_locales_tac false ctxt [])
+           (fn ctxt => Locale.intro_locales_tac {strict = true, eager = false} ctxt [])
            (full_name, expr) end;
 
     fun declare_declinfo updates lthy phi ctxt =
diff -r c77efde4e4fd -r 0c1d7a414185 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 19 16:11:54 2018 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 19 20:45:47 2018 +0200
@@ -782,7 +782,8 @@
 
 fun standard_intro_classes_tac ctxt facts st =
   if null facts andalso not (Thm.no_prems st) then
-    (intro_classes_tac ctxt [] ORELSE Locale.intro_locales_tac true ctxt []) st
+    (intro_classes_tac ctxt [] ORELSE
+      Locale.intro_locales_tac {strict = true, eager = true} ctxt []) st
   else no_tac st;
 
 fun standard_tac ctxt facts =
diff -r c77efde4e4fd -r 0c1d7a414185 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Wed Sep 19 16:11:54 2018 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Sep 19 20:45:47 2018 +0200
@@ -79,8 +79,7 @@
   val witness_add: attribute
   val intro_add: attribute
   val unfold_add: attribute
-  val intro_locales_tac: bool -> Proof.context -> thm list -> tactic
-  val try_intro_locales_tac: bool -> Proof.context -> thm list -> tactic
+  val intro_locales_tac: {strict: bool, eager: bool} -> Proof.context -> thm list -> tactic
 
   (* Registrations and dependencies *)
   type registration = {dep: string * morphism, mixin: (morphism * bool) option, export: morphism}
@@ -701,17 +700,16 @@
 
 (* Tactics *)
 
-fun gen_intro_locales_tac intros_tac eager ctxt =
-  intros_tac ctxt
+fun intro_locales_tac {strict, eager} ctxt =
+  (if strict then Method.intros_tac else Method.try_intros_tac) ctxt
     (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 _ = Theory.setup
- (Method.setup \<^binding>\<open>intro_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac false))
+ (Method.setup \<^binding>\<open>intro_locales\<close>
+    (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = false}))
     "back-chain introduction rules of locales without unfolding predicates" #>
-  Method.setup \<^binding>\<open>unfold_locales\<close> (Scan.succeed (METHOD o try_intro_locales_tac true))
+  Method.setup \<^binding>\<open>unfold_locales\<close>
+    (Scan.succeed (METHOD o intro_locales_tac {strict = false, eager = true}))
     "back-chain all introduction rules of locales");