1.1 --- a/src/Pure/Isar/proof_context.ML Sun Oct 25 19:14:46 2009 +0100
1.2 +++ b/src/Pure/Isar/proof_context.ML Sun Oct 25 19:17:42 2009 +0100
1.3 @@ -21,7 +21,10 @@
1.4 val restore_mode: Proof.context -> Proof.context -> Proof.context
1.5 val abbrev_mode: Proof.context -> bool
1.6 val set_stmt: bool -> Proof.context -> Proof.context
1.7 + val local_naming: Name_Space.naming
1.8 + val map_naming: (Name_Space.naming -> Name_Space.naming) -> Proof.context -> Proof.context
1.9 val naming_of: Proof.context -> Name_Space.naming
1.10 + val restore_naming: Proof.context -> Proof.context -> Proof.context
1.11 val full_name: Proof.context -> binding -> string
1.12 val consts_of: Proof.context -> Consts.T
1.13 val const_syntax_name: Proof.context -> string -> string
1.14 @@ -92,11 +95,6 @@
1.15 val get_fact_single: Proof.context -> Facts.ref -> thm
1.16 val get_thms: Proof.context -> xstring -> thm list
1.17 val get_thm: Proof.context -> xstring -> thm
1.18 - val add_path: string -> Proof.context -> Proof.context
1.19 - val mandatory_path: string -> Proof.context -> Proof.context
1.20 - val conceal: Proof.context -> Proof.context
1.21 - val restore_naming: Proof.context -> Proof.context -> Proof.context
1.22 - val reset_naming: Proof.context -> Proof.context
1.23 val note_thmss: string -> (Thm.binding * (thm list * attribute list) list) list ->
1.24 Proof.context -> (string * thm list) list * Proof.context
1.25 val put_thms: bool -> string * thm list option -> Proof.context -> Proof.context
1.26 @@ -232,6 +230,7 @@
1.27 map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
1.28
1.29 val naming_of = #naming o rep_context;
1.30 +val restore_naming = map_naming o K o naming_of
1.31 val full_name = Name_Space.full_name o naming_of;
1.32
1.33 val syntax_of = #syntax o rep_context;
1.34 @@ -923,15 +922,6 @@
1.35 end;
1.36
1.37
1.38 -(* name space operations *)
1.39 -
1.40 -val add_path = map_naming o Name_Space.add_path;
1.41 -val mandatory_path = map_naming o Name_Space.mandatory_path;
1.42 -val conceal = map_naming Name_Space.conceal;
1.43 -val restore_naming = map_naming o K o naming_of;
1.44 -val reset_naming = map_naming (K local_naming);
1.45 -
1.46 -
1.47 (* facts *)
1.48
1.49 local