src/HOL/Statespace/state_space.ML

         val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
         val rule = DistinctTreeProver.distinct_implProver ctxt distinct_thm goal;
       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)
   end;
 

 
     fun interprete_parent (prefix, (_, pname, rs)) =
       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 =
       let
         fun upd_prf ctxt =