# HG changeset patch
# User wenzelm
# Date 1332325519 -3600
# Node ID 355317493f34d04f9bff890500e8c34c8b9324a7
# Parent  e2741ec9ae361ed647fec57a43c39def85d5d3f8
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
tuned;

diff -r e2741ec9ae36 -r 355317493f34 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Mar 21 11:00:34 2012 +0100
+++ b/src/Pure/Isar/class.ML	Wed Mar 21 11:25:19 2012 +0100
@@ -512,6 +512,8 @@
 
 fun instantiation (tycos, vs, sort) thy =
   let
+    val naming = Sign.naming_of thy;
+
     val _ = if null tycos then error "At least one arity must be given" else ();
     val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
     fun get_param tyco (param, (_, (c, ty))) =
@@ -545,7 +547,7 @@
     |> Overloading.activate_improvable_syntax
     |> Context.proof_map (Syntax_Phases.term_check 0 "resorting" resort_check)
     |> synchronize_inst_syntax
-    |> Local_Theory.init NONE ""
+    |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
diff -r e2741ec9ae36 -r 355317493f34 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Wed Mar 21 11:00:34 2012 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 21 11:25:19 2012 +0100
@@ -49,7 +49,7 @@
   val class_alias: binding -> class -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
-  val init: serial option -> string -> operations -> Proof.context -> local_theory
+  val init: Name_Space.naming -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val exit: local_theory -> Proof.context
   val exit_global: local_theory -> theory
@@ -78,13 +78,11 @@
 
 datatype lthy = LThy of
  {naming: Name_Space.naming,
-  theory_prefix: string,
   operations: operations,
   target: Proof.context};
 
-fun make_lthy (naming, theory_prefix, operations, target) =
-  LThy {naming = naming, theory_prefix = theory_prefix,
-    operations = operations, target = target};
+fun make_lthy (naming, operations, target) =
+  LThy {naming = naming, operations = operations, target = target};
 
 
 (* context data *)
@@ -101,8 +99,8 @@
   | SOME (LThy data) => data);
 
 fun map_lthy f lthy =
-  let val {naming, theory_prefix, operations, target} = get_lthy lthy
-  in Data.put (SOME (make_lthy (f (naming, theory_prefix, operations, target)))) lthy end;
+  let val {naming, operations, target} = get_lthy lthy
+  in Data.put (SOME (make_lthy (f (naming, operations, target)))) lthy end;
 
 val affirm = tap get_lthy;
 
@@ -112,8 +110,7 @@
 val naming_of = #naming o get_lthy;
 val full_name = Name_Space.full_name o naming_of;
 
-fun map_naming f = map_lthy (fn (naming, theory_prefix, operations, target) =>
-  (f naming, theory_prefix, operations, target));
+fun map_naming f = map_lthy (fn (naming, operations, target) => (f naming, operations, target));
 
 val conceal = map_naming Name_Space.conceal;
 val new_group = map_naming Name_Space.new_group;
@@ -126,8 +123,7 @@
 
 val target_of = #target o get_lthy;
 
-fun map_target f = map_lthy (fn (naming, theory_prefix, operations, target) =>
-  (naming, theory_prefix, operations, f target));
+fun map_target f = map_lthy (fn (naming, operations, target) => (naming, operations, f target));
 
 
 (* substructure mappings *)
@@ -192,8 +188,7 @@
 (* primitive operations *)
 
 fun operation f lthy = f (#operations (get_lthy lthy)) lthy;
-fun operation1 f x = operation (fn ops => f ops x);
-fun operation2 f x y lthy = operation (fn ops => f ops x y) lthy;
+fun operation2 f x y = operation (fn ops => f ops x y);
 
 val pretty = operation #pretty;
 val abbrev = apsnd checkpoint ooo operation2 #abbrev;
@@ -246,21 +241,15 @@
 
 (* init *)
 
-fun init group theory_prefix operations target =
-  let val naming =
-    Sign.naming_of (Proof_Context.theory_of target)
-    |> Name_Space.set_group group
-    |> Name_Space.mandatory_path theory_prefix;
-  in
-    target |> Data.map
-      (fn NONE => SOME (make_lthy (naming, theory_prefix, operations, target))
-        | SOME _ => error "Local theory already initialized")
-    |> checkpoint
-  end;
+fun init naming operations target =
+  target |> Data.map
+    (fn NONE => SOME (make_lthy (naming, operations, target))
+      | SOME _ => error "Local theory already initialized")
+  |> checkpoint;
 
 fun restore lthy =
-  let val {naming, theory_prefix, operations, target} = get_lthy lthy
-  in init (Name_Space.get_group naming) theory_prefix operations target end;
+  let val {naming, operations, target} = get_lthy lthy
+  in init naming operations target end;
 
 
 (* exit *)
diff -r e2741ec9ae36 -r 355317493f34 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Wed Mar 21 11:00:34 2012 +0100
+++ b/src/Pure/Isar/named_target.ML	Wed Mar 21 11:25:19 2012 +0100
@@ -192,11 +192,13 @@
 fun init before_exit target thy =
   let
     val ta = named_target thy target before_exit;
+    val naming = Sign.naming_of thy
+      |> Name_Space.mandatory_path (Long_Name.base_name target);
   in
     thy
     |> init_context ta
     |> Data.put (SOME ta)
-    |> Local_Theory.init NONE (Long_Name.base_name target)
+    |> Local_Theory.init naming
        {define = Generic_Target.define (target_foundation ta),
         notes = Generic_Target.notes (target_notes ta),
         abbrev = Generic_Target.abbrev (target_abbrev ta),
diff -r e2741ec9ae36 -r 355317493f34 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Mar 21 11:00:34 2012 +0100
+++ b/src/Pure/Isar/overloading.ML	Wed Mar 21 11:25:19 2012 +0100
@@ -189,6 +189,7 @@
 fun gen_overloading prep_const raw_overloading thy =
   let
     val ctxt = Proof_Context.init_global thy;
+    val naming = Sign.naming_of thy;
     val _ = if null raw_overloading then error "At least one parameter must be given" else ();
     val overloading = raw_overloading |> map (fn (v, const, checked) =>
       (Term.dest_Const (prep_const ctxt const), (v, checked)));
@@ -200,7 +201,7 @@
     |> fold (fn ((_, ty), (v, _)) => Variable.declare_names (Free (v, ty))) overloading
     |> activate_improvable_syntax
     |> synchronize_syntax
-    |> Local_Theory.init NONE ""
+    |> Local_Theory.init naming
        {define = Generic_Target.define foundation,
         notes = Generic_Target.notes
           (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),