src/HOL/Statespace/state_space.ML

                       DistinctTreeProver.mk_tree (fn n => Free (n,nameT)) nameT
                                 (sort fast_string_ord all_comps)),
                       ([]))])];
 
   in thy
-     |> Locale.add_locale_i "" name vars [assumes]
+     |> Locale.add_locale "" name vars [assumes]
      ||> ProofContext.theory_of
      ||> interprete_parent name dist_thm_full_name parent_expr
      |> #2
   end;
 

   in thy
      |> namespace_definition
            (suffix namespaceN name) nameT parents_expr
            (map fst parent_comps) (map fst components)
      |> Context.theory_map (add_statespace full_name args parents components [])
-     |> Locale.add_locale_i "" (suffix valuetypesN name) (Locale.Merge locs)
+     |> Locale.add_locale "" (suffix valuetypesN name) (Locale.Merge locs)
             [Element.Constrains constrains]
      |> ProofContext.theory_of o #2
      |> fold interprete_parent_valuetypes parents
-     |> Locale.add_locale "" name
+     |> Locale.add_locale_cmd name
               (Locale.Merge [Locale.Locale (suffix namespaceN full_name)
                             ,Locale.Locale (suffix valuetypesN full_name)]) fixestate
      |> ProofContext.theory_of o #2
      |> fold interprete_parent parents
      |> add_declaration (SOME full_name) (declare_declinfo components')