Ahere to modern naming conventions; proper treatment of internal vs external names.

--- a/src/FOL/ex/NewLocaleSetup.thy	Fri Nov 28 11:55:46 2008 +0100
+++ b/src/FOL/ex/NewLocaleSetup.thy	Fri Nov 28 12:26:14 2008 +0100
@@ -28,7 +28,7 @@
     (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin
       >> (fn ((name, (expr, elems)), begin) =>
           (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
-            (Expression.add_locale name name expr elems #-> TheoryTarget.begin)));
+            (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin)));
 
 val _ =
   OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag

--- a/src/Pure/Isar/expression.ML	Fri Nov 28 11:55:46 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Fri Nov 28 12:26:14 2008 +0100
@@ -19,19 +19,20 @@
     Proof.context -> (term * term list) list list * Proof.context;
 
   (* Declaring locales *)
-  val add_locale: string -> bstring -> expression -> Element.context list -> theory ->
+  val add_locale_cmd: string -> bstring -> expression -> Element.context list -> theory ->
     string * Proof.context
-  val add_locale_i: string -> bstring -> expression_i -> Element.context_i list -> theory ->
+  val add_locale: string -> bstring -> expression_i -> Element.context_i list -> theory ->
     string * Proof.context
 
   (* Interpretation *)
-  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
+  val sublocale_cmd: (thm list list -> Proof.context -> Proof.context) ->
     string -> expression -> theory -> Proof.state;
-  val sublocale_i: (thm list list -> Proof.context -> Proof.context) ->
+  val sublocale: (thm list list -> Proof.context -> Proof.context) ->
     string -> expression_i -> theory -> Proof.state;
 
   (* Debugging and development *)
   val parse_expression: OuterParse.token list -> expression * OuterParse.token list
+    (* FIXME to spec_parse.ML *)
 end;
 
 
@@ -776,8 +777,8 @@
 
 in
 
-val add_locale = gen_add_locale read_declaration;
-val add_locale_i = gen_add_locale cert_declaration;
+val add_locale_cmd = gen_add_locale read_declaration;
+val add_locale = gen_add_locale cert_declaration;
 
 end;
 
@@ -796,19 +797,19 @@
 
 local
 
-fun gen_sublocale prep_expr
-    after_qed target expression thy =
+fun gen_sublocale prep_expr intern
+    after_qed raw_target expression thy =
   let
+    val target = intern thy raw_target;
     val target_ctxt = NewLocale.init target thy;
-    val target' = NewLocale.intern thy target;
 
     val ((propss, deps, export'), goal_ctxt) = prep_expr expression target_ctxt;
     
-    fun store_dep target ((name, morph), thms) =
+    fun store_dep ((name, morph), thms) =
       NewLocale.add_dependency target (name, morph $> Element.satisfy_morphism thms $> export');
 
     fun after_qed' results =
-      fold (store_dep target') (deps ~~ prep_result propss results) #>
+      fold store_dep (deps ~~ prep_result propss results) #>
       after_qed results;
 
   in
@@ -819,8 +820,8 @@
 
 in
 
-fun sublocale x = gen_sublocale read_goal_expression x;
-fun sublocale_i x = gen_sublocale cert_goal_expression x;
+fun sublocale_cmd x = gen_sublocale read_goal_expression NewLocale.intern x;
+fun sublocale x = gen_sublocale cert_goal_expression (K I) x;
 
 end;
 

--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 28 11:55:46 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 28 12:26:14 2008 +0100
@@ -403,7 +403,7 @@
     "prove sublocale relation between a locale and a locale expression" K.thy_goal
     (P.xname --| (P.$$$ "\\<subseteq>" || P.$$$ "<") -- P.!!! Expression.parse_expression
       >> (fn (loc, expr) =>
-        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale (K I) loc expr))));
+        Toplevel.print o (Toplevel.theory_to_proof (Expression.sublocale_cmd (K I) loc expr))));
 
 val _ =
   OuterSyntax.command "interpretation"

--- a/src/Pure/Isar/new_locale.ML	Fri Nov 28 11:55:46 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Fri Nov 28 12:26:14 2008 +0100
@@ -198,9 +198,8 @@
 
 fun roundup thy activate_dep (name, morph) (marked, ctxt) =
   let
-    val name' = intern thy name;
-    val Loc {dependencies, ...} = the_locale thy name';
-    val (dependencies', marked') = add thy 0 (name', morph) ([], marked);
+    val Loc {dependencies, ...} = the_locale thy name;
+    val (dependencies', marked') = add thy 0 (name, morph) ([], marked);
   in
     (marked', ctxt |> fold_rev (activate_dep thy) dependencies')
   end;
@@ -234,9 +233,8 @@
 
 fun activate name thy activ_elem input =
   let
-    val name' = intern thy name;
     val Loc {parameters = (_, params), spec = (asm, defs), dependencies, ...} =
-      the_locale thy name';
+      the_locale thy name;
   in
     input |>
       (if not (null params) then activ_elem (Fixes params) else I) |>
@@ -245,7 +243,7 @@
       (if not (null defs)
         then activ_elem (Defines (map (fn def => (Attrib.no_binding, (def, []))) defs))
         else I) |>
-      pair empty |> roundup thy (activate_notes activ_elem) (name', Morphism.identity) |> snd
+      pair empty |> roundup thy (activate_notes activ_elem) (name, Morphism.identity) |> snd
   end;
 
 
@@ -287,10 +285,12 @@
 fun init name thy = activate name thy init_elem (ProofContext.init thy);
 
 fun print_locale thy show_facts name =
-  let val ctxt = init name thy
+  let
+    val name' = intern thy name;
+    val ctxt = init name' thy
   in
     Pretty.big_list "locale elements:"
-      (activate name thy (cons_elem show_facts) [] |> rev |> 
+      (activate name' thy (cons_elem show_facts) [] |> rev |> 
         map (Element.pretty_ctxt ctxt) |> map Pretty.chunks) |> Pretty.writeln
   end