adjusted locale signature to *_cmd convention

--- a/src/HOL/Statespace/state_space.ML	Mon Nov 17 17:00:21 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Mon Nov 17 17:00:22 2008 +0100
@@ -311,7 +311,7 @@
                       ([]))])];
 
   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
@@ -457,11 +457,11 @@
            (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

--- a/src/Pure/Isar/isar_syn.ML	Mon Nov 17 17:00:21 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Nov 17 17:00:22 2008 +0100
@@ -394,7 +394,7 @@
     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (Locale.empty, []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Locale.add_locale "" name expr elems #-> TheoryTarget.begin)));
+            (Locale.add_locale_cmd name expr elems #-> TheoryTarget.begin)));
 
 val opt_prefix = Scan.optional (P.binding --| P.$$$ ":") Name.no_binding;
 
@@ -406,7 +406,7 @@
       opt_prefix  -- SpecParse.locale_expr -- SpecParse.locale_insts
         >> (fn ((name, expr), insts) => Toplevel.print o
             Toplevel.theory_to_proof
-              (Locale.interpretation I (true, Name.name_of name) expr insts #> snd)));
+              (Locale.interpretation_cmd (Name.name_of name) expr insts)));
 
 val _ =
   OuterSyntax.command "interpret"
@@ -415,7 +415,7 @@
     (opt_prefix -- SpecParse.locale_expr -- SpecParse.locale_insts
       >> (fn ((name, expr), insts) => Toplevel.print o
           Toplevel.proof'
-            (fn int => Locale.interpret Seq.single (true, Name.name_of name) expr insts int #> snd)));
+            (fn int => Locale.interpret_cmd (Name.name_of name) expr insts int)));
 
 
 (* classes *)

--- a/src/Pure/Isar/specification.ML	Mon Nov 17 17:00:21 2008 +0100
+++ b/src/Pure/Isar/specification.ML	Mon Nov 17 17:00:22 2008 +0100
@@ -368,7 +368,7 @@
 in
 
 val theorem = gen_theorem (K I) Locale.cert_context_statement;
-val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement_i;
+val theorem_cmd = gen_theorem Attrib.intern_src Locale.read_context_statement;
 
 fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));