src/Pure/Isar/local_theory.ML
changeset 33724 5ee13e0428d2
parent 33671 4b0f2599ed48
child 33764 7bcefaab8d41
     1.1 --- a/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:48:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Tue Nov 17 14:50:55 2009 +0100
     1.3 @@ -14,7 +14,8 @@
     1.4    val full_name: local_theory -> binding -> string
     1.5    val map_naming: (Name_Space.naming -> Name_Space.naming) -> local_theory -> local_theory
     1.6    val conceal: local_theory -> local_theory
     1.7 -  val set_group: serial -> local_theory -> local_theory
     1.8 +  val new_group: local_theory -> local_theory
     1.9 +  val reset_group: local_theory -> local_theory
    1.10    val restore_naming: local_theory -> local_theory -> local_theory
    1.11    val target_of: local_theory -> Proof.context
    1.12    val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
    1.13 @@ -42,7 +43,7 @@
    1.14    val term_syntax: bool -> declaration -> local_theory -> local_theory
    1.15    val declaration: bool -> declaration -> local_theory -> local_theory
    1.16    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
    1.17 -  val init: string -> operations -> Proof.context -> local_theory
    1.18 +  val init: serial option -> string -> operations -> Proof.context -> local_theory
    1.19    val restore: local_theory -> local_theory
    1.20    val reinit: local_theory -> local_theory
    1.21    val exit: local_theory -> Proof.context
    1.22 @@ -114,7 +115,8 @@
    1.23    (f naming, theory_prefix, operations, target));
    1.24  
    1.25  val conceal = map_naming Name_Space.conceal;
    1.26 -val set_group = map_naming o Name_Space.set_group;
    1.27 +val new_group = map_naming Name_Space.new_group;
    1.28 +val reset_group = map_naming Name_Space.reset_group;
    1.29  
    1.30  val restore_naming = map_naming o K o naming_of;
    1.31  
    1.32 @@ -203,9 +205,10 @@
    1.33  
    1.34  (* init *)
    1.35  
    1.36 -fun init theory_prefix operations target =
    1.37 +fun init group theory_prefix operations target =
    1.38    let val naming =
    1.39      Sign.naming_of (ProofContext.theory_of target)
    1.40 +    |> Name_Space.set_group group
    1.41      |> Name_Space.mandatory_path theory_prefix;
    1.42    in
    1.43      target |> Data.map
    1.44 @@ -215,8 +218,8 @@
    1.45    end;
    1.46  
    1.47  fun restore lthy =
    1.48 -  let val {theory_prefix, operations, target, ...} = get_lthy lthy
    1.49 -  in init theory_prefix operations target end;
    1.50 +  let val {naming, theory_prefix, operations, target} = get_lthy lthy
    1.51 +  in init (Name_Space.get_group naming) theory_prefix operations target end;
    1.52  
    1.53  val reinit = checkpoint o operation #reinit;
    1.54