src/Pure/sign.ML
changeset 59886 e0dc738eb08c
parent 59880 30687c3f2b10
child 59896 e563b0ee0331
     1.1 --- a/src/Pure/sign.ML	Tue Mar 31 21:12:22 2015 +0200
     1.2 +++ b/src/Pure/sign.ML	Tue Mar 31 22:31:05 2015 +0200
     1.3 @@ -101,6 +101,8 @@
     1.4      (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory
     1.5    val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory
     1.6    val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory
     1.7 +  val get_scope: theory -> Binding.scope option
     1.8 +  val new_scope: theory -> Binding.scope * theory
     1.9    val new_group: theory -> theory
    1.10    val reset_group: theory -> theory
    1.11    val add_path: string -> theory -> theory
    1.12 @@ -500,6 +502,14 @@
    1.13  
    1.14  (* naming *)
    1.15  
    1.16 +val get_scope = Name_Space.get_scope o naming_of;
    1.17 +
    1.18 +fun new_scope thy =
    1.19 +  let
    1.20 +    val (scope, naming') = Name_Space.new_scope (naming_of thy);
    1.21 +    val thy' = map_naming (K naming') thy;
    1.22 +  in (scope, thy') end;
    1.23 +
    1.24  val new_group = map_naming Name_Space.new_group;
    1.25  val reset_group = map_naming Name_Space.reset_group;
    1.26