# HG changeset patch
# User wenzelm
# Date 1258469730 -3600
# Node ID b424b3259966a998f137fd90cfcd05a1e8e0c603
# Parent  e441fede163d2c9a36ea4efbefe548fda1c7a282# Parent  e2d5d7f51aa335b4529284f4ceec65201a14020a
merged

diff -r e441fede163d -r b424b3259966 src/HOL/Extraction.thy
--- a/src/HOL/Extraction.thy	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Extraction.thy	Tue Nov 17 15:55:30 2009 +0100
@@ -13,20 +13,6 @@
 subsection {* Setup *}
 
 setup {*
-let
-fun realizes_set_proc (Const ("realizes", Type ("fun", [Type ("Null", []), _])) $ r $
-      (Const ("op :", _) $ x $ S)) = (case strip_comb S of
-        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, U), ts @ [x]))
-      | (Free (s, U), ts) => SOME (list_comb (Free (s, U), ts @ [x]))
-      | _ => NONE)
-  | realizes_set_proc (Const ("realizes", Type ("fun", [T, _])) $ r $
-      (Const ("op :", _) $ x $ S)) = (case strip_comb S of
-        (Var (ixn, U), ts) => SOME (list_comb (Var (ixn, T --> U), r :: ts @ [x]))
-      | (Free (s, U), ts) => SOME (list_comb (Free (s, T --> U), r :: ts @ [x]))
-      | _ => NONE)
-  | realizes_set_proc _ = NONE;
-
-in
   Extraction.add_types
       [("bool", ([], NONE))] #>
   Extraction.set_preprocessor (fn thy =>
@@ -35,7 +21,6 @@
       Proofterm.rewrite_proof thy
         (RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
       ProofRewriteRules.elim_vars (curry Const @{const_name default}))
-end
 *}
 
 lemmas [extraction_expand] =
diff -r e441fede163d -r b424b3259966 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -568,7 +568,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy4) =
       thy3
       |> Sign.map_naming Name_Space.conceal
-      |> Inductive.add_inductive_global (serial ())
+      |> Inductive.add_inductive_global
           {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
@@ -1511,7 +1511,7 @@
     val ({intrs = rec_intrs, elims = rec_elims, raw_induct = rec_induct, ...}, thy11) =
       thy10
       |> Sign.map_naming Name_Space.conceal
-      |> Inductive.add_inductive_global (serial ())
+      |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
diff -r e441fede163d -r b424b3259966 src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -239,7 +239,7 @@
 
 local
 
-fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
+fun gen_primrec prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
   let
     val (fixes', spec) = fst (prep_spec (raw_fixes @ raw_params) raw_spec lthy);
     val fixes = List.take (fixes', length raw_fixes);
@@ -280,7 +280,6 @@
       else primrec_err ("functions " ^ commas_quote names2 ^
         "\nare not mutually recursive");
     val (defs_thms, lthy') = lthy |>
-      set_group ? Local_Theory.set_group (serial ()) |>
       fold_map (apfst (snd o snd) oo Local_Theory.define Thm.definitionK o fst) defs';
     val qualify = Binding.qualify false
       (space_implode "_" (map (Long_Name.base_name o #1) defs));
@@ -384,8 +383,8 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_spec (K I);
-val add_primrec_cmd = gen_primrec true Specification.read_spec Syntax.read_term;
+val add_primrec = gen_primrec Specification.check_spec (K I);
+val add_primrec_cmd = gen_primrec Specification.read_spec Syntax.read_term;
 
 end;
 
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -155,7 +155,7 @@
     val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) =
       thy0
       |> Sign.map_naming Name_Space.conceal
-      |> Inductive.add_inductive_global (serial ())
+      |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name',
             coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -174,7 +174,7 @@
     val ({raw_induct = rep_induct, intrs = rep_intrs, ...}, thy2) =
       thy1
       |> Sign.map_naming Name_Space.conceal
-      |> Inductive.add_inductive_global (serial ())
+      |> Inductive.add_inductive_global
           {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
            coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/Function/fun.ML
--- a/src/HOL/Tools/Function/fun.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -151,15 +151,11 @@
   domintros=false, partials=false, tailrec=false }
 
 fun gen_fun add config fixes statements int lthy =
-  let val group = serial () in
-    lthy
-      |> Local_Theory.set_group group
-      |> add fixes statements config
-      |> by_pat_completeness_auto int
-      |> Local_Theory.restore
-      |> Local_Theory.set_group group
-      |> termination_by (Function_Common.get_termination_prover lthy) int
-  end;
+  lthy
+    |> add fixes statements config
+    |> by_pat_completeness_auto int
+    |> Local_Theory.restore
+    |> termination_by (Function_Common.get_termination_prover lthy) int
 
 val add_fun = gen_fun Function.add_function
 val add_fun_cmd = gen_fun Function.add_function_cmd
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Function/function.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -20,8 +20,6 @@
 
     val termination_proof : term option -> local_theory -> Proof.state
     val termination_proof_cmd : string option -> local_theory -> Proof.state
-    val termination : term option -> local_theory -> Proof.state
-    val termination_cmd : string option -> local_theory -> Proof.state
 
     val setup : theory -> theory
     val get_congs : Proof.context -> thm list
@@ -119,7 +117,6 @@
         end
     in
       lthy
-        |> is_external ? Local_Theory.set_group (serial ())
         |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
         |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
     end
@@ -170,18 +167,8 @@
       |> Proof.theorem_i NONE afterqed [[(goal, [])]]
     end
 
-val termination_proof = gen_termination_proof Syntax.check_term;
-val termination_proof_cmd = gen_termination_proof Syntax.read_term;
-
-fun termination term_opt lthy =
-  lthy
-  |> Local_Theory.set_group (serial ())
-  |> termination_proof term_opt;
-
-fun termination_cmd term_opt lthy =
-  lthy
-  |> Local_Theory.set_group (serial ())
-  |> termination_proof_cmd term_opt;
+val termination_proof = gen_termination_proof Syntax.check_term
+val termination_proof_cmd = gen_termination_proof Syntax.read_term
 
 
 (* Datatype hook to declare datatype congs as "function_congs" *)
@@ -217,13 +204,13 @@
 val _ =
   OuterSyntax.local_theory_to_proof "function" "define general recursive functions" K.thy_goal
   (function_parser default_config
-     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config));
+     >> (fn ((config, fixes), statements) => add_function_cmd fixes statements config))
 
 val _ =
   OuterSyntax.local_theory_to_proof "termination" "prove termination of a recursive function" K.thy_goal
-  (Scan.option P.term >> termination_cmd);
+  (Scan.option P.term >> termination_proof_cmd)
 
-end;
+end
 
 
 end
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -354,7 +354,7 @@
             val (ind_result, thy') =
               thy
               |> Sign.map_naming Name_Space.conceal
-              |> Inductive.add_inductive_global (serial ())
+              |> Inductive.add_inductive_global
                 {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
                   no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
                 (map (fn (s, T) =>
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -51,7 +51,7 @@
     (Attrib.binding * string) list ->
     (Facts.ref * Attrib.src list) list ->
     bool -> local_theory -> inductive_result * local_theory
-  val add_inductive_global: serial -> inductive_flags ->
+  val add_inductive_global: inductive_flags ->
     ((binding * typ) * mixfix) list -> (string * typ) list -> (Attrib.binding * term) list ->
     thm list -> theory -> inductive_result * theory
   val arities_of: thm -> (string * int) list
@@ -886,19 +886,17 @@
       coind = coind, no_elim = false, no_ind = false, skip_mono = false, fork_mono = not int};
   in
     lthy
-    |> Local_Theory.set_group (serial ())
     |> gen_add_inductive_i mk_def flags cs (map (apfst Binding.name_of o fst) ps) intrs monos
   end;
 
 val add_inductive_i = gen_add_inductive_i add_ind_def;
 val add_inductive = gen_add_inductive add_ind_def;
 
-fun add_inductive_global group flags cnames_syn pnames pre_intros monos thy =
+fun add_inductive_global flags cnames_syn pnames pre_intros monos thy =
   let
     val name = Sign.full_name thy (fst (fst (hd cnames_syn)));
     val ctxt' = thy
       |> Theory_Target.init NONE
-      |> Local_Theory.set_group group
       |> add_inductive_i flags cnames_syn pnames pre_intros monos |> snd
       |> Local_Theory.exit;
     val info = #2 (the_inductive ctxt' name);
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -350,7 +350,7 @@
     (** realizability predicate **)
 
     val (ind_info, thy3') = thy2 |>
-      Inductive.add_inductive_global (serial ())
+      Inductive.add_inductive_global
         {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
           no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
diff -r e441fede163d -r b424b3259966 src/HOL/Tools/primrec.ML
--- a/src/HOL/Tools/primrec.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOL/Tools/primrec.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -265,7 +265,7 @@
 
 local
 
-fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
+fun gen_primrec prep_spec raw_fixes raw_spec lthy =
   let
     val (fixes, spec) = fst (prep_spec raw_fixes raw_spec lthy);
     fun attr_bindings prefix = map (fn ((b, attrs), _) =>
@@ -275,7 +275,6 @@
         map (Attrib.internal o K) [Simplifier.simp_add, Nitpick_Simps.add]);
   in
     lthy
-    |> set_group ? Local_Theory.set_group (serial ())
     |> add_primrec_simple fixes (map snd spec)
     |-> (fn (prefix, simps) => fold_map Local_Theory.note (attr_bindings prefix ~~ simps)
       #-> (fn simps' => Local_Theory.note (simp_attr_binding prefix, maps snd simps')))
@@ -284,8 +283,8 @@
 
 in
 
-val add_primrec = gen_primrec false Specification.check_spec;
-val add_primrec_cmd = gen_primrec true Specification.read_spec;
+val add_primrec = gen_primrec Specification.check_spec;
+val add_primrec_cmd = gen_primrec Specification.read_spec;
 
 end;
 
diff -r e441fede163d -r b424b3259966 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -421,7 +421,6 @@
 (* code adapted from HOL/Tools/primrec.ML *)
 
 fun gen_fixrec
-  (set_group : bool)
   prep_spec
   (strict : bool)
   raw_fixes
@@ -473,8 +472,8 @@
 
 in
 
-val add_fixrec = gen_fixrec false Specification.check_spec;
-val add_fixrec_cmd = gen_fixrec true Specification.read_spec;
+val add_fixrec = gen_fixrec Specification.check_spec;
+val add_fixrec_cmd = gen_fixrec Specification.read_spec;
 
 end; (* local *)
 
diff -r e441fede163d -r b424b3259966 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/General/name_space.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -34,8 +34,11 @@
   type naming
   val default_naming: naming
   val conceal: naming -> naming
-  val set_group: serial -> naming -> naming
+  val get_group: naming -> serial option
+  val set_group: serial option -> naming -> naming
   val set_theory_name: string -> naming -> naming
+  val new_group: naming -> naming
+  val reset_group: naming -> naming
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
@@ -241,12 +244,18 @@
 val conceal = map_naming (fn (_, group, theory_name, path) =>
   (true, group, theory_name, path));
 
-fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
-  (conceal, SOME group, theory_name, path));
-
 fun set_theory_name theory_name = map_naming (fn (conceal, group, _, path) =>
   (conceal, group, theory_name, path));
 
+
+fun get_group (Naming {group, ...}) = group;
+
+fun set_group group = map_naming (fn (conceal, _, theory_name, path) =>
+  (conceal, group, theory_name, path));
+
+fun new_group naming = set_group (SOME (serial ())) naming;
+val reset_group = set_group NONE;
+
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
 val parent_path = map_path (perhaps (try (#1 o split_last)));
diff -r e441fede163d -r b424b3259966 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -14,7 +14,8 @@
   val full_name: local_theory -> binding -> string
   val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
   val conceal: local_theory -> local_theory
-  val set_group: serial -> local_theory -> local_theory
+  val new_group: local_theory -> local_theory
+  val reset_group: local_theory -> local_theory
   val restore_naming: local_theory -> local_theory -> local_theory
   val target_of: local_theory -> Proof.context
   val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
@@ -42,7 +43,7 @@
   val term_syntax: bool -> declaration -> local_theory -> local_theory
   val declaration: bool -> declaration -> local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val init: string -> operations -> Proof.context -> local_theory
+  val init: serial option -> string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
   val exit: local_theory -> Proof.context
@@ -114,7 +115,8 @@
   (f naming, theory_prefix, operations, target));
 
 val conceal = map_naming Name_Space.conceal;
-val set_group = map_naming o Name_Space.set_group;
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
 
 val restore_naming = map_naming o K o naming_of;
 
@@ -203,9 +205,10 @@
 
 (* init *)
 
-fun init theory_prefix operations target =
+fun init group theory_prefix operations target =
   let val naming =
     Sign.naming_of (ProofContext.theory_of target)
+    |> Name_Space.set_group group
     |> Name_Space.mandatory_path theory_prefix;
   in
     target |> Data.map
@@ -215,8 +218,8 @@
   end;
 
 fun restore lthy =
-  let val {theory_prefix, operations, target, ...} = get_lthy lthy
-  in init theory_prefix operations target end;
+  let val {naming, theory_prefix, operations, target} = get_lthy lthy
+  in init (Name_Space.get_group naming) theory_prefix operations target end;
 
 val reinit = checkpoint o operation #reinit;
 
diff -r e441fede163d -r b424b3259966 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -324,7 +324,7 @@
 
 fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   Data.put ta #>
-  Local_Theory.init (Long_Name.base_name target)
+  Local_Theory.init NONE (Long_Name.base_name target)
    {pretty = pretty ta,
     abbrev = abbrev ta,
     define = define ta,
diff -r e441fede163d -r b424b3259966 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -302,7 +302,8 @@
 local
 
 fun apply_tr int (Init (_, f, exit)) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
+      State (SOME (Theory (Context.Theory
+          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
       State (NONE, prev)
   | apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
@@ -419,7 +420,13 @@
     | _ => raise UNDEF));
 
 fun theory' f = transaction (fn int =>
-  (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (f int thy), NONE)
+  (fn Theory (Context.Theory thy, _) =>
+      let val thy' = thy
+        |> Sign.new_group
+        |> Theory.checkpoint
+        |> f int
+        |> Sign.reset_group;
+      in Theory (Context.Theory thy', NONE) end
     | _ => raise UNDEF));
 
 fun theory f = theory' (K f);
@@ -442,7 +449,10 @@
   (fn Theory (gthy, _) =>
         let
           val finish = loc_finish loc gthy;
-          val lthy' = f int (loc_begin loc gthy);
+          val lthy' = loc_begin loc gthy
+            |> Local_Theory.new_group
+            |> f int
+            |> Local_Theory.reset_group;
         in Theory (finish lthy', SOME lthy') end
     | _ => raise UNDEF));
 
@@ -491,14 +501,14 @@
 in
 
 fun local_theory_to_proof' loc f = begin_proof
-  (fn int => fn gthy => f int (loc_begin loc gthy))
-  (loc_finish loc);
+  (fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy)))
+  (fn gthy => loc_finish loc gthy o Local_Theory.reset_group);
 
 fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f);
 
 fun theory_to_proof f = begin_proof
-  (K (fn Context.Theory thy => f thy | _ => raise UNDEF))
-  (K (Context.Theory o ProofContext.theory_of));
+  (K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF))
+  (K (Context.Theory o Sign.reset_group o ProofContext.theory_of));
 
 end;
 
@@ -531,7 +541,7 @@
 
 fun skip_proof_to_theory pred = transaction (fn _ =>
   (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF
-  | _ => raise UNDEF));
+    | _ => raise UNDEF));
 
 
 
diff -r e441fede163d -r b424b3259966 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Tue Nov 17 14:10:31 2009 +0100
+++ b/src/Pure/sign.ML	Tue Nov 17 15:55:30 2009 +0100
@@ -121,6 +121,8 @@
   val del_trrules: (xstring * string) Syntax.trrule list -> theory -> theory
   val add_trrules_i: ast Syntax.trrule list -> theory -> theory
   val del_trrules_i: ast Syntax.trrule list -> theory -> theory
+  val new_group: theory -> theory
+  val reset_group: theory -> theory
   val add_path: string -> theory -> theory
   val root_path: theory -> theory
   val parent_path: theory -> theory
@@ -610,6 +612,9 @@
 
 (* naming *)
 
+val new_group = map_naming Name_Space.new_group;
+val reset_group = map_naming Name_Space.reset_group;
+
 val add_path = map_naming o Name_Space.add_path;
 val root_path = map_naming Name_Space.root_path;
 val parent_path = map_naming Name_Space.parent_path;