src/HOL/Statespace/state_space.ML

         val goal = List.nth (cprems_of st,i-1);
         val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
       in EVERY [rtac rule i] st
       end
 
-    fun tac ctxt = EVERY [NewLocale.intro_locales_tac true ctxt [],
+    fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [],
                           ALLGOALS (SUBGOAL (solve_tac ctxt))]
 
   in thy
      |> prove_interpretation_in tac (name,parent_expr)
   end;

 
     fun interprete_parent (_, pname, rs) =
       let
         val expr = ([(pname, (("",false), Expression.Positional rs))],[])
       in prove_interpretation_in
-           (fn ctxt => NewLocale.intro_locales_tac false ctxt [])
+           (fn ctxt => Locale.intro_locales_tac false ctxt [])
            (full_name, expr) end;
 
     fun declare_declinfo updates lthy phi ctxt =
       let
         fun upd_prf ctxt =