--- a/src/Pure/sign.ML Tue Mar 31 21:12:22 2015 +0200
+++ b/src/Pure/sign.ML Tue Mar 31 22:31:05 2015 +0200
@@ -101,6 +101,8 @@
(string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
+ val get_scope: theory -> Binding.scope option
+ val new_scope: theory -> Binding.scope * theory
val new_group: theory -> theory
val reset_group: theory -> theory
val add_path: string -> theory -> theory
@@ -500,6 +502,14 @@
(* naming *)
+val get_scope = Name_Space.get_scope o naming_of;
+
+fun new_scope thy =
+ let
+ val (scope, naming') = Name_Space.new_scope (naming_of thy);
+ val thy' = map_naming (K naming') thy;
+ in (scope, thy') end;
+
val new_group = map_naming Name_Space.new_group;
val reset_group = map_naming Name_Space.reset_group;