# HG changeset patch
# User wenzelm
# Date 1303062844 -7200
# Node ID 774df7c59508dd9b1f2a75273a43812987adba8a
# Parent  b9a6b465da25850aecf547693f3eab3d89728bec
report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;

diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -177,7 +177,7 @@
           SOME t => (((name, t), log_builtin thy name t), thy)
         | NONE =>
             thy
-            |> Sign.declare_const ((Binding.name isa_name, T),
+            |> Sign.declare_const_global ((Binding.name isa_name, T),
                  mk_syntax name arity)
             |> (fn (t, thy') => (((name, t), log_new thy' name t), thy'))))
   fun declare (name, ((Ts, T), atts)) =
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/HOLCF/Tools/Domain/domain.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -44,7 +44,7 @@
 
 fun add_arity ((b, sorts, mx), sort) thy : theory =
   thy
-  |> Sign.add_types [(b, length sorts, mx)]
+  |> Sign.add_types_global [(b, length sorts, mx)]
   |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
 
 fun gen_add_domain
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -39,9 +39,9 @@
     val rep_bind = Binding.suffix_name "_rep" dbind
 
     val (abs_const, thy) =
-        Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy
+        Sign.declare_const_global ((abs_bind, rhsT ->> lhsT), NoSyn) thy
     val (rep_const, thy) =
-        Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy
+        Sign.declare_const_global ((rep_bind, lhsT ->> rhsT), NoSyn) thy
 
     val x = Free ("x", lhsT)
     val y = Free ("y", rhsT)
@@ -98,7 +98,7 @@
     (* declare new types *)
     fun thy_type (dbind, mx, (lhsT, _)) =
         (dbind, (length o snd o dest_Type) lhsT, mx)
-    val thy = Sign.add_types (map thy_type dom_eqns) thy
+    val thy = Sign.add_types_global (map thy_type dom_eqns) thy
 
     (* axiomatize type constructor arities *)
     fun thy_arity (_, _, (lhsT, _)) =
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -264,7 +264,7 @@
   val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
   val bisim_type = R_types ---> boolT
   val (bisim_const, thy) =
-      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy
+      Sign.declare_const_global ((bisim_bind, bisim_type), NoSyn) thy
 
   (* define bisimulation predicate *)
   local
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -239,7 +239,7 @@
     : (term * thm) * theory =
   let
     val typ = Term.fastype_of rhs
-    val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy
+    val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
     val eqn = Logic.mk_equals (const, rhs)
     val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn)
     val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
@@ -276,7 +276,7 @@
         val map_type = mapT lhsT
         val map_bind = Binding.suffix_name "_map" tbind
       in
-        Sign.declare_const ((map_bind, map_type), NoSyn) thy
+        Sign.declare_const_global ((map_bind, map_type), NoSyn) thy
       end
     val (map_consts, thy) = thy |>
       fold_map declare_map_const (dbinds ~~ dom_eqns)
@@ -417,7 +417,7 @@
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Theory.copy |>
-      Sign.add_types (map (fn (tvs, tbind, mx, _, morphs) =>
+      Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
         (tbind, length tvs, mx)) doms_raw)
 
     fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
@@ -499,7 +499,7 @@
         val defl_type =
           map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT
       in
-        Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
+        Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy
       end
     val (defl_consts, thy) =
       fold_map declare_defl_const (defl_flagss ~~ doms) thy
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -262,7 +262,7 @@
         val take_type = HOLogic.natT --> lhsT ->> lhsT
         val take_bind = Binding.suffix_name "_take" dbind
         val (take_const, thy) =
-          Sign.declare_const ((take_bind, take_type), NoSyn) thy
+          Sign.declare_const_global ((take_bind, take_type), NoSyn) thy
         val take_eqn = Logic.mk_equals (take_const, take_rhs)
         val (take_def_thm, thy) =
             add_qualified_def "take_def" (dbind, take_eqn) thy
@@ -401,7 +401,7 @@
         val finite_type = lhsT --> boolT
         val finite_bind = Binding.suffix_name "_finite" dbind
         val (finite_const, thy) =
-          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy
+          Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy
         val x = Free ("x", lhsT)
         val n = Free ("n", natT)
         val finite_rhs =
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -194,7 +194,7 @@
 
     val tmp_thy = thy |>
       Theory.copy |>
-      Sign.add_types (map (fn (tvs, tname, mx, _) =>
+      Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
         (Binding.name tname, length tvs, mx)) dts);
 
     val atoms = atoms_of thy;
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -649,7 +649,7 @@
     (* this theory is used just for parsing *)
     val tmp_thy = thy |>
       Theory.copy |>
-      Sign.add_types (map (fn (tvs, tname, mx, _) =>
+      Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
         (tname, length tvs, mx)) dts);
 
     val (tyvars, _, _, _)::_ = dts;
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -321,7 +321,7 @@
                 fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
           val ([def_thm], thy') =
             thy
-            |> Sign.declare_const decl |> snd
+            |> Sign.declare_const_global decl |> snd
             |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
 
         in (defs @ [def_thm], thy')
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -96,16 +96,16 @@
     val name_of = fst o dest_Const
     val thy = Proof_Context.theory_of ctxt |> Context.reject_draft
     val (maybe_t, thy) =
-      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
+      Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
                           Mixfix (maybe_mixfix (), [1000], 1000)) thy
     val (abs_t, thy) =
-      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
+      Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
                           Mixfix (abs_mixfix (), [40], 40)) thy
     val (base_t, thy) =
-      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
+      Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
                           Mixfix (base_mixfix (), [1000], 1000)) thy
     val (step_t, thy) =
-      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
+      Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
                           Mixfix (step_mixfix (), [1000], 1000)) thy
   in
     (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -295,8 +295,9 @@
 
     val thy1' = thy1 |>
       Theory.copy |>
-      Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
-        Extraction.add_typeof_eqns_i ty_eqs;
+      Sign.add_types_global
+        (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
+      Extraction.add_typeof_eqns_i ty_eqs;
     val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
       SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
 
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/record.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -153,7 +153,7 @@
 
     val ([isom_def], cdef_thy) =
       typ_thy
-      |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
+      |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
       |> Global_Theory.add_defs false
         [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
 
@@ -1648,7 +1648,7 @@
 
     fun mk_defs () =
       typ_thy
-      |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
+      |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
       |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
       ||> Theory.checkpoint
     val ([ext_def], defs_thy) =
@@ -2087,9 +2087,9 @@
       |> Typedecl.abbrev_global
         (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
       |> Sign.qualified_path false binding
-      |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
+      |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
         (sel_decls ~~ (field_syntax @ [NoSyn]))
-      |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
+      |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
         (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
       |> (Global_Theory.add_defs false o
             map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
diff -r b9a6b465da25 -r 774df7c59508 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/HOL/Tools/typedef.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -92,7 +92,7 @@
         (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
   in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
 
-fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A thy =
+fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A lthy =
   let
     (* errors *)
 
@@ -111,18 +111,20 @@
 
     (* axiomatization *)
 
-    val ((RepC, AbsC), consts_thy) = thy
-      |> Sign.declare_const ((Rep_name, newT --> oldT), NoSyn)
-      ||>> Sign.declare_const ((Abs_name, oldT --> newT), NoSyn);
+    val ((RepC, AbsC), consts_lthy) = lthy
+      |> Local_Theory.background_theory_result
+        (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
+          Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
 
     val typedef_deps = Term.add_consts A [];
 
-    val ((axiom_name, axiom), axiom_thy) = consts_thy
-      |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
-      ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
-      ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
+    val ((axiom_name, axiom), axiom_lthy) = consts_lthy
+      |> Local_Theory.background_theory_result
+        (Thm.add_axiom consts_lthy (typedef_name, mk_typedef newT oldT RepC AbsC A) ##>
+          Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
+          Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
 
-  in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
+  in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
 
 
 (* prepare_typedef *)
@@ -185,9 +187,8 @@
           Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
           ||> Thm.term_of;
 
-        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
-          Local_Theory.background_theory_result
-            (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
+        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy
+          |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A;
 
         val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy);
         val typedef =
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/General/name_space.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -46,10 +46,10 @@
   val qualified_path: bool -> binding -> naming -> naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
-  val declare: bool -> naming -> binding -> T -> string * T
+  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
   val alias: naming -> binding -> string -> T -> T
   type 'a table = T * 'a Symtab.table
-  val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
+  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   val empty_table: string -> 'a table
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
@@ -335,7 +335,7 @@
             err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
     in (kind, internals, entries') end);
 
-fun declare strict naming binding space =
+fun declare ctxt strict naming binding space =
   let
     val Naming {group, theory_name, ...} = naming;
     val (concealed, spec) = name_spec naming binding;
@@ -344,15 +344,17 @@
     val name = Long_Name.implode (map fst spec);
     val _ = name = "" andalso err_bad binding;
 
+    val pos = Position.default (Binding.pos_of binding);
     val entry =
      {concealed = concealed,
       group = group,
       theory_name = theory_name,
-      pos = Position.default (Binding.pos_of binding),
+      pos = pos,
       id = serial ()};
     val space' = space
       |> fold (add_name name) accs
       |> new_entry strict (name, (accs', entry));
+    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
   in (name, space') end;
 
 
@@ -379,8 +381,8 @@
 
 type 'a table = T * 'a Symtab.table;
 
-fun define strict naming (binding, x) (space, tab) =
-  let val (name, space') = declare strict naming binding space
+fun define ctxt strict naming (binding, x) (space, tab) =
+  let val (name, space') = declare ctxt strict naming binding space
   in (name, (space', Symtab.update (name, x) tab)) end;
 
 fun empty_table kind = (empty kind, Symtab.empty);
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -83,7 +83,9 @@
   end;
 
 fun add_attribute name att comment thy = thy
-  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
+  |> Attributes.map
+    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
+      (name, (att, comment)) #> snd);
 
 
 (* name space *)
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/class.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -326,9 +326,9 @@
       |> map_types Type.strip_sorts;
   in
     thy
-    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
+    |> Sign.declare_const_global ((b, Type.strip_sorts ty'), mx)
     |> snd
-    |> Thm.add_def false false (b_def, def_eq)
+    |> Thm.add_def_global false false (b_def, def_eq)
     |>> apsnd Thm.varifyT_global
     |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm)
       #> snd
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/class_declaration.ML
--- a/src/Pure/Isar/class_declaration.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/class_declaration.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -253,7 +253,7 @@
         val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
       in
         thy
-        |> Sign.declare_const ((b, ty0), syn)
+        |> Sign.declare_const_global ((b, ty0), syn)
         |> snd
         |> pair ((Variable.name b, ty), (c, ty'))
       end;
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/code.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -339,21 +339,23 @@
 
 fun build_tsig thy =
   let
-    val (tycos, _) = (the_signatures o the_exec) thy;
-    val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
+    val ctxt = Syntax.init_pretty_global thy;
+    val (tycos, _) = the_signatures (the_exec thy);
+    val decls = #types (Type.rep_tsig (Sign.tsig_of thy))
       |> snd 
       |> Symtab.fold (fn (tyco, n) =>
           Symtab.update (tyco, Type.LogicalType n)) tycos;
   in
     Type.empty_tsig
-    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming
+    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type ctxt Name_Space.default_naming
         (Binding.qualified_name tyco, n) | _ => I) decls
   end;
 
-fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
+fun cert_signature thy =
+  Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
 
-fun read_signature thy = cert_signature thy o Type.strip_sorts
-  o Syntax.parse_typ (Proof_Context.init_global thy);
+fun read_signature thy =
+  cert_signature thy o Type.strip_sorts o Syntax.parse_typ (Proof_Context.init_global thy);
 
 fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -648,7 +648,7 @@
     val ([pred_def], defs_thy) =
       thy
       |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
-      |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
+      |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
       |> Global_Theory.add_defs false
         [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
     val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -198,11 +198,12 @@
 
 fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
   let
-    val (const, lthy2) = lthy |> Local_Theory.background_theory_result
-      (Sign.declare_const ((b, U), mx));
+    val (const, lthy2) = lthy
+      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
     val lhs = list_comb (const, type_params @ term_params);
-    val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result
-      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
+    val ((_, def), lthy3) = lthy2
+      |> Local_Theory.background_theory_result
+        (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
   in ((lhs, def), lthy3) end;
 
 fun theory_notes kind global_facts lthy =
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -129,7 +129,7 @@
 val _ =
   Outer_Syntax.command "nonterminal"
     "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
-    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
+    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
 val _ =
   Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/locale.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -173,7 +173,7 @@
   | NONE => error ("Unknown locale " ^ quote name));
 
 fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
-  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
+  thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
     (binding,
       mk_locale ((parameters, spec, intros, axioms),
         ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/method.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -344,7 +344,9 @@
   end;
 
 fun add_method name meth comment thy = thy
-  |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
+  |> Methods.map
+    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
+      (name, (meth, comment)) #> snd);
 
 
 (* get methods *)
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/object_logic.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -89,7 +89,7 @@
   let val c = Sign.full_name thy b in
     thy
     |> add_consts [(b, T, mx)]
-    |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
+    |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
     |> map_data (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
         else (base_sort, SOME c, atomize_rulify))
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/overloading.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -143,7 +143,8 @@
 
 fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
   Local_Theory.background_theory_result
-    (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
+    (Thm.add_def_global (not checked) true
+      (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   ##> Local_Theory.target synchronize_syntax
   #-> (fn (_, def) => pair (Const (c, U), def))
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -906,7 +906,7 @@
 
 fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
   | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
-      (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
+      (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
 
 in
 
@@ -1033,7 +1033,7 @@
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
-      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (b, t);
+      |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
   in
     ctxt
     |> (map_consts o apfst) (K consts')
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -180,7 +180,7 @@
 
     (*axioms*)
     val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
-        fold_map Thm.add_axiom
+        fold_map Thm.add_axiom_global
           (map (apfst (fn a => Binding.map_name (K a) b))
             (Global_Theory.name_multi (Variable.name b) (map subst props)))
         #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Isar/typedecl.ML
--- a/src/Pure/Isar/typedecl.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Isar/typedecl.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -40,8 +40,9 @@
     |> pair name
   end;
 
-fun basic_typedecl (b, n, mx) =
-  basic_decl (fn name => Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) (b, n, mx);
+fun basic_typedecl (b, n, mx) lthy =
+  basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
+    (b, n, mx) lthy;
 
 
 (* global type -- without dependencies on type parameters of the context *)
@@ -91,7 +92,7 @@
       handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   in
     lthy
-    |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
+    |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
     |> snd
     |> pair name
   end;
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Proof/extraction.ML
--- a/src/Pure/Proof/extraction.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Proof/extraction.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -36,7 +36,7 @@
   thy
   |> Theory.copy
   |> Sign.root_path
-  |> Sign.add_types [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
+  |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
   |> Sign.add_consts
       [(Binding.name "typeof", "'b::{} => Type", NoSyn),
        (Binding.name "Type", "'a::{} itself => Type", NoSyn),
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -45,8 +45,8 @@
   |> Theory.copy
   |> Sign.root_path
   |> Sign.set_defsort []
-  |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
-  |> fold (snd oo Sign.declare_const)
+  |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
+  |> fold (snd oo Sign.declare_const_global)
       [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
        ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
        ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
@@ -55,7 +55,7 @@
        ((Binding.name "Oracle", propT --> proofT), NoSyn),
        ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
        ((Binding.name "MinProof", proofT), Delimfix "?")]
-  |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
+  |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
   |> Sign.add_syntax_i
       [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
        ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/axclass.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -384,9 +384,9 @@
   in
     thy
     |> Sign.qualified_path true (Binding.name name_inst)
-    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
+    |> Sign.declare_const_global ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) =>
-      Thm.add_def false true
+      Thm.add_def_global false true
         (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
       #>> apsnd Thm.varifyT_global
       #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
@@ -405,7 +405,7 @@
     val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   in
     thy
-    |> Thm.add_def false false (b', prop)
+    |> Thm.add_def_global false false (b', prop)
     |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
   end;
 
@@ -608,7 +608,7 @@
     val names = name args;
   in
     thy
-    |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
+    |> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs)
     |-> fold (add o Drule.export_without_context o snd)
   end;
 
@@ -631,13 +631,14 @@
     thy
     |> Sign.primitive_class (bclass, super)
     |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
-    |> Theory.add_deps "" (class_const class) (map class_const super)
+    |> Theory.add_deps_global "" (class_const class) (map class_const super)
   end;
 
 in
 
 val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
+val axiomatize_class_cmd =
+  ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
 val axiomatize_classrel = ax_classrel cert_classrel;
 val axiomatize_classrel_cmd = ax_classrel read_classrel;
 val axiomatize_arity = ax_arity Proof_Context.cert_arity;
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/consts.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -29,9 +29,9 @@
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
   val instance: T -> string * typ list -> typ
-  val declare: Name_Space.naming -> binding * typ -> T -> T
+  val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
   val constrain: string * typ option -> T -> T
-  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
+  val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
     binding * term -> T -> (term * term) * T
   val revert_abbrev: string -> string -> T -> T
   val hide: bool -> string -> T -> T
@@ -231,12 +231,12 @@
 
 (* declarations *)
 
-fun declare naming (b, declT) =
+fun declare ctxt naming (b, declT) =
   map_consts (fn (decls, constraints, rev_abbrevs) =>
     let
       val decl = {T = declT, typargs = typargs_of declT};
       val _ = Binding.check b;
-      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
+      val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
     in (decls', constraints, rev_abbrevs) end);
 
 
@@ -267,8 +267,9 @@
 
 in
 
-fun abbreviate pp tsig naming mode (b, raw_rhs) consts =
+fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   let
+    val pp = Syntax.pp ctxt;
     val cert_term = certify pp tsig false consts;
     val expand_term = certify pp tsig true consts;
     val force_expand = mode = Print_Mode.internal;
@@ -290,7 +291,7 @@
         val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
         val _ = Binding.check b;
         val (_, decls') = decls
-          |> Name_Space.define true naming (b, (decl, SOME abbr));
+          |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
         val rev_abbrevs' = rev_abbrevs
           |> update_abbrevs mode (rev_abbrev lhs rhs);
       in (decls', constraints, rev_abbrevs') end)
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/facts.ML
--- a/src/Pure/facts.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/facts.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -32,9 +32,10 @@
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
-  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
-  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
-  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
+  val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
+  val add_dynamic: Proof.context -> Name_Space.naming ->
+    binding * (Context.generic -> thm list) -> T -> string * T
   val del: string -> T -> T
   val hide: bool -> string -> T -> T
 end;
@@ -190,11 +191,11 @@
 
 local
 
-fun add strict do_props naming (b, ths) (Facts {facts, props}) =
+fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
   let
     val (name, facts') =
       if Binding.is_empty b then ("", facts)
-      else Name_Space.define strict naming (b, Static ths) facts;
+      else Name_Space.define ctxt strict naming (b, Static ths) facts;
     val props' =
       if do_props
       then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
@@ -203,16 +204,16 @@
 
 in
 
-val add_global = add true false;
-val add_local = add false;
+fun add_global ctxt = add ctxt true false;
+fun add_local ctxt = add ctxt false;
 
 end;
 
 
 (* add dynamic entries *)
 
-fun add_dynamic naming (b, f) (Facts {facts, props}) =
-  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
+fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
+  let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
   in (name, make_facts facts' props) end;
 
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/global_theory.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -140,7 +140,9 @@
       val (thy', thms') =
         register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
       val thms'' = map (Thm.transfer thy') thms';
-      val thy'' = thy' |> (Data.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
+      val thy'' = thy'
+        |> (Data.map o apfst)
+            (Facts.add_global (Proof_Context.init_global thy') naming (b, thms'') #> snd);
     in (thms'', thy'') end;
 
 
@@ -176,7 +178,7 @@
 
 fun add_thms_dynamic (b, f) thy = thy
   |> (Data.map o apfst)
-      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
+      (Facts.add_dynamic (Proof_Context.init_global thy) (Sign.naming_of thy) (b, f) #> snd);
 
 
 (* note_thmss *)
@@ -200,14 +202,15 @@
 
 fun no_read _ (_, t) = t;
 
-fun read thy (b, str) =
-  Syntax.read_prop_global thy str handle ERROR msg =>
+fun read ctxt (b, str) =
+  Syntax.read_prop ctxt str handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
 
 fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   let
-    val prop = prep thy (b, raw_prop);
-    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+    val ctxt = Syntax.init_pretty_global thy;
+    val prop = prep ctxt (b, raw_prop);
+    val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
     val thm = def
       |> Thm.forall_intr_frees
       |> Thm.forall_elim_vars 0
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/more_thm.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -63,8 +63,10 @@
   val forall_intr_frees: thm -> thm
   val unvarify_global: thm -> thm
   val close_derivation: thm -> thm
-  val add_axiom: binding * term -> theory -> (string * thm) * theory
-  val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
+  val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
+  val add_axiom_global: binding * term -> theory -> (string * thm) * theory
+  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
+  val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   type attribute = Context.generic * thm -> Context.generic * thm
   type binding = binding * attribute list
   val empty_binding: binding
@@ -346,17 +348,17 @@
     val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
   in (strip, recover, t') end;
 
-fun add_axiom (b, prop) thy =
+fun add_axiom ctxt (b, prop) thy =
   let
     val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
 
-    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
+    val _ = Sign.no_vars ctxt prop;
     val (strip, recover, prop') = stripped_sorts thy prop;
     val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
     val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
 
-    val thy' =
-      Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
+    val thy' = thy
+      |> Theory.add_axiom ctxt (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
     val axm_name = Sign.full_name thy' b';
     val axm' = Thm.axiom thy' axm_name;
     val thm =
@@ -365,13 +367,15 @@
       |> fold elim_implies of_sorts;
   in ((axm_name, thm), thy') end;
 
-fun add_def unchecked overloaded (b, prop) thy =
+fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
+
+fun add_def ctxt unchecked overloaded (b, prop) thy =
   let
-    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
+    val _ = Sign.no_vars ctxt prop;
     val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
     val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
 
-    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
+    val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
     val axm_name = Sign.full_name thy' b;
     val axm' = Thm.axiom thy' axm_name;
     val thm =
@@ -380,6 +384,9 @@
       |> fold_rev Thm.implies_intr prems;
   in ((axm_name, thm), thy') end;
 
+fun add_def_global unchecked overloaded arg thy =
+  add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy;
+
 
 
 (** attributes **)
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/pure_thy.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -55,12 +55,12 @@
 val _ = Context.>> (Context.map_theory
   (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
    Old_Appl_Syntax.put false #>
-   Sign.add_types
+   Sign.add_types_global
    [(Binding.name "fun", 2, NoSyn),
     (Binding.name "prop", 0, NoSyn),
     (Binding.name "itself", 1, NoSyn),
     (Binding.name "dummy", 0, NoSyn)]
-  #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
+  #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
   #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
   #> Sign.add_syntax_i
    [("",            typ "prop' => prop",               Delimfix "_"),
@@ -177,11 +177,11 @@
     (Binding.name "prop", typ "prop => prop", NoSyn),
     (Binding.name "TYPE", typ "'a itself", NoSyn),
     (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
-  #> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
-  #> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
-  #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
-  #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
-  #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
+  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
+  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
+  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
+  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
+  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   #> Sign.add_trfuns Syntax_Trans.pure_trfuns
   #> Sign.local_path
   #> Sign.add_consts_i
@@ -199,6 +199,7 @@
   #> Sign.hide_const false "Pure.sort_constraint"
   #> Sign.hide_const false "Pure.conjunction"
   #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
-  #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
+  #> fold (fn (a, prop) =>
+      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
 
 end;
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/sign.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -67,9 +67,11 @@
   val cert_prop: theory -> term -> term
   val no_frees: Proof.context -> term -> term
   val no_vars: Proof.context -> term -> term
-  val add_types: (binding * int * mixfix) list -> theory -> theory
-  val add_nonterminals: binding list -> theory -> theory
-  val add_type_abbrev: binding * string list * typ -> theory -> theory
+  val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
+  val add_types_global: (binding * int * mixfix) list -> theory -> theory
+  val add_nonterminals: Proof.context -> binding list -> theory -> theory
+  val add_nonterminals_global: binding list -> theory -> theory
+  val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
   val add_syntax: (string * string * mixfix) list -> theory -> theory
   val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
   val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
@@ -78,7 +80,8 @@
   val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
-  val declare_const: (binding * typ) * mixfix -> theory -> term * theory
+  val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
+  val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
   val add_consts: (binding * string * mixfix) list -> theory -> theory
   val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
   val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
@@ -325,25 +328,31 @@
 
 (* add type constructors *)
 
-fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
+fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   let
     fun type_syntax (b, n, mx) =
       (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
     val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
-    val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
+    val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
   in (naming, syn', tsig', consts) end);
 
+fun add_types_global types thy =
+  add_types (Syntax.init_pretty_global thy) types thy;
+
 
 (* add nonterminals *)
 
-fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
-  (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
+fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
+  (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
+
+fun add_nonterminals_global ns thy =
+  add_nonterminals (Syntax.init_pretty_global thy) ns thy;
 
 
 (* add type abbreviations *)
 
-fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
-  (naming, syn, Type.add_abbrev naming abbr tsig, consts));
+fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
+  (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
 
 
 (* modify syntax *)
@@ -385,9 +394,8 @@
 
 local
 
-fun gen_add_consts parse_typ raw_args thy =
+fun gen_add_consts parse_typ ctxt raw_args thy =
   let
-    val ctxt = Proof_Context.init_global thy;
     val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
     fun prep (b, raw_T, mx) =
       let
@@ -399,23 +407,27 @@
     val args = map prep raw_args;
   in
     thy
-    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
+    |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
     |> add_syntax_i (map #2 args)
     |> pair (map #3 args)
   end;
 
 in
 
-fun add_consts args = snd o gen_add_consts Syntax.parse_typ args;
-fun add_consts_i args = snd o gen_add_consts (K I) args;
+fun add_consts args thy =
+  #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy);
+fun add_consts_i args thy =
+  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
 
-fun declare_const ((b, T), mx) thy =
+fun declare_const ctxt ((b, T), mx) thy =
   let
     val pos = Binding.pos_of b;
-    val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
+    val ([const as Const (c, _)], thy') = gen_add_consts (K I) ctxt [(b, T, mx)] thy;
     val _ = Position.report pos (Markup.const_decl c);
   in (const, thy') end;
 
+fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
+
 end;
 
 
@@ -428,7 +440,7 @@
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
       handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val (res, consts') = consts_of thy
-      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of thy) (naming_of thy) mode (b, t);
+      |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
   in (res, thy |> map_consts (K consts')) end;
 
 fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
@@ -450,7 +462,8 @@
 fun primitive_class (bclass, classes) thy =
   thy |> map_sign (fn (naming, syn, tsig, consts) =>
     let
-      val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
+      val ctxt = Syntax.init_pretty_global thy;
+      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
     in (naming, syn, tsig', consts) end)
   |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/simplifier.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -197,13 +197,15 @@
        proc = proc,
        identifier = identifier};
   in
-    lthy |> Local_Theory.declaration false (fn phi =>
+    lthy |> Local_Theory.declaration false (fn phi => fn context =>
       let
         val b' = Morphism.binding phi b;
         val simproc' = morph_simproc phi simproc;
       in
-        Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
-        #> map_ss (fn ss => ss addsimprocs [simproc'])
+        context
+        |> Simprocs.map
+          (#2 o Name_Space.define (Context.proof_of context) true naming (b', simproc'))
+        |> map_ss (fn ss => ss addsimprocs [simproc'])
       end)
   end;
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/theory.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -28,9 +28,10 @@
   val at_end: (theory -> theory option) -> theory -> theory
   val begin_theory: string -> theory list -> theory
   val end_theory: theory -> theory
-  val add_axiom: binding * term -> theory -> theory
-  val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
-  val add_def: bool -> bool -> binding * term -> theory -> theory
+  val add_axiom: Proof.context -> binding * term -> theory -> theory
+  val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
+  val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
+  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
   val add_finals_i: bool -> term list -> theory -> theory
   val add_finals: bool -> string list -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
@@ -154,37 +155,35 @@
 
 (* raw axioms *)
 
-fun cert_axm thy (b, raw_tm) =
+fun cert_axm ctxt (b, raw_tm) =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val t = Sign.cert_prop thy raw_tm
       handle TYPE (msg, _, _) => error msg
         | TERM (msg, _) => error msg;
     val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
 
-    val ctxt = Syntax.init_pretty_global thy
-      |> Config.put show_sorts true;
     val bad_sorts =
       rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
     val _ = null bad_sorts orelse
       error ("Illegal sort constraints in primitive specification: " ^
-        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
-  in
-    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
-  end handle ERROR msg =>
+        commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
+  in (b, Sign.no_vars ctxt t) end
+  handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
 
-fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
+fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   let
-    val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
-    val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
+    val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
+    val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
   in axioms' end);
 
 
 (* dependencies *)
 
-fun dependencies thy unchecked def description lhs rhs =
+fun dependencies ctxt unchecked def description lhs rhs =
   let
-    val ctxt = Syntax.init_pretty_global thy;
+    val thy = Proof_Context.theory_of ctxt;
     val consts = Sign.consts_of thy;
     fun prep const =
       let val Const (c, T) = Sign.no_vars ctxt (Const const)
@@ -200,26 +199,29 @@
         "\nThe error(s) above occurred in " ^ quote description);
   in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
 
-fun add_deps a raw_lhs raw_rhs thy =
+fun add_deps ctxt a raw_lhs raw_rhs thy =
   let
     val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
     val description = if a = "" then #1 lhs ^ " axiom" else a;
-  in thy |> map_defs (dependencies thy false NONE description lhs rhs) end;
+  in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
+
+fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
 
 fun specify_const decl thy =
-  let val (t as Const const, thy') = Sign.declare_const decl thy
-  in (t, add_deps "" const [] thy') end;
+  let val (t as Const const, thy') = Sign.declare_const_global decl thy;
+  in (t, add_deps_global "" const [] thy') end;
 
 
 (* overloading *)
 
-fun check_overloading thy overloaded (c, T) =
+fun check_overloading ctxt overloaded (c, T) =
   let
+    val thy = Proof_Context.theory_of ctxt;
+
     val declT = Sign.the_const_constraint thy c
       handle TYPE (msg, _, _) => error msg;
     val T' = Logic.varifyT_global T;
 
-    val ctxt = Syntax.init_pretty_global thy;
     fun message sorts txt =
       [Pretty.block [Pretty.str "Specification of constant ",
         Pretty.str c, Pretty.str " ::", Pretty.brk 1,
@@ -238,27 +240,27 @@
 
 local
 
-fun check_def thy unchecked overloaded (b, tm) defs =
+fun check_def ctxt unchecked overloaded (b, tm) defs =
   let
-    val ctxt = Proof_Context.init_global thy;
+    val thy = Proof_Context.theory_of ctxt;
     val name = Sign.full_name thy b;
     val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);
     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
-    val _ = check_overloading thy overloaded lhs_const;
-  in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
+    val _ = check_overloading ctxt overloaded lhs_const;
+  in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
    [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
-    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
+    Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
 
 in
 
-fun add_def unchecked overloaded raw_axm thy =
-  let val axm = cert_axm thy raw_axm in
+fun add_def ctxt unchecked overloaded raw_axm thy =
+  let val axm = cert_axm ctxt raw_axm in
     thy
-    |> map_defs (check_def thy unchecked overloaded axm)
-    |> add_axiom axm
+    |> map_defs (check_def ctxt unchecked overloaded axm)
+    |> add_axiom ctxt axm
   end;
 
 end;
@@ -270,18 +272,20 @@
 
 fun gen_add_finals prep_term overloaded args thy =
   let
+    val ctxt = Syntax.init_pretty_global thy;
     fun const_of (Const const) = const
       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
       | const_of _ = error "Attempt to finalize non-constant term";
-    fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
-    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
-      Sign.cert_term thy o prep_term thy;
+    fun specify (c, T) = dependencies ctxt false NONE (c ^ " axiom") (c, T) [];
+    val finalize =
+      specify o tap (check_overloading ctxt overloaded) o const_of o
+        Sign.cert_term thy o prep_term ctxt;
   in thy |> map_defs (fold finalize args) end;
 
 in
 
 val add_finals_i = gen_add_finals (K I);
-val add_finals = gen_add_finals Syntax.read_term_global;
+val add_finals = gen_add_finals Syntax.read_term;
 
 end;
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/thm.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -1740,7 +1740,8 @@
 fun add_oracle (b, oracle) thy =
   let
     val naming = Sign.naming_of thy;
-    val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
+    val (name, tab') =
+      Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
     val thy' = Oracles.put tab' thy;
   in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
 
diff -r b9a6b465da25 -r 774df7c59508 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Apr 17 13:47:22 2011 +0200
+++ b/src/Pure/type.ML	Sun Apr 17 19:54:04 2011 +0200
@@ -86,12 +86,13 @@
   val eq_type: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
-  val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
+  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
+    binding * class list -> tsig -> tsig
   val hide_class: bool -> string -> tsig -> tsig
   val set_defsort: sort -> tsig -> tsig
-  val add_type: Name_Space.naming -> binding * int -> tsig -> tsig
-  val add_abbrev: Name_Space.naming -> binding * string list * typ -> tsig -> tsig
-  val add_nonterminal: Name_Space.naming -> binding -> tsig -> tsig
+  val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
+  val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
+  val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   val hide_type: bool -> string -> tsig -> tsig
   val add_arity: Pretty.pp -> arity -> tsig -> tsig
   val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
@@ -576,13 +577,13 @@
 
 (* classes *)
 
-fun add_class pp naming (c, cs) tsig =
+fun add_class ctxt pp naming (c, cs) tsig =
   tsig |> map_tsig (fn ((space, classes), default, types) =>
     let
       val cs' = map (cert_class tsig) cs
         handle TYPE (msg, _, _) => error msg;
       val _ = Binding.check c;
-      val (c', space') = space |> Name_Space.declare true naming c;
+      val (c', space') = space |> Name_Space.declare ctxt true naming c;
       val classes' = classes |> Sorts.add_class pp (c', cs');
     in ((space', classes'), default, types) end);
 
@@ -626,8 +627,8 @@
 
 local
 
-fun new_decl naming (c, decl) types =
-  (Binding.check c; #2 (Name_Space.define true naming (c, decl) types));
+fun new_decl ctxt naming (c, decl) types =
+  (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
 
 fun map_types f = map_tsig (fn (classes, default, types) =>
   let
@@ -643,11 +644,11 @@
 
 in
 
-fun add_type naming (c, n) =
+fun add_type ctxt naming (c, n) =
   if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
-  else map_types (new_decl naming (c, LogicalType n));
+  else map_types (new_decl ctxt naming (c, LogicalType n));
 
-fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
+fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   let
     fun err msg =
       cat_error msg ("The error(s) above occurred in type abbreviation " ^
@@ -662,9 +663,9 @@
       (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
         [] => []
       | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
-  in types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
+  in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
 
-fun add_nonterminal naming = map_types o new_decl naming o rpair Nonterminal;
+fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
 
 end;