report Name_Space.declare/define, relatively to context;
authorwenzelm
Sun Apr 17 19:54:04 2011 +0200 (2011-04-17)
changeset 42375774df7c59508
parent 42374 b9a6b465da25
child 42376 c3abf2c3f541
report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/HOLCF/Tools/Domain/domain.ML
src/HOL/HOLCF/Tools/Domain/domain_axioms.ML
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_declaration.ML
src/Pure/Isar/code.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/typedecl.ML
src/Pure/Proof/extraction.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/axclass.ML
src/Pure/consts.ML
src/Pure/facts.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
src/Pure/sign.ML
src/Pure/simplifier.ML
src/Pure/theory.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Apr 17 13:47:22 2011 +0200
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Apr 17 19:54:04 2011 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4            SOME t => (((name, t), log_builtin thy name t), thy)
     1.5          | NONE =>
     1.6              thy
     1.7 -            |> Sign.declare_const ((Binding.name isa_name, T),
     1.8 +            |> Sign.declare_const_global ((Binding.name isa_name, T),
     1.9                   mk_syntax name arity)
    1.10              |> (fn (t, thy') => (((name, t), log_new thy' name t), thy'))))
    1.11    fun declare (name, ((Ts, T), atts)) =
     2.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Apr 17 13:47:22 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Sun Apr 17 19:54:04 2011 +0200
     2.3 @@ -44,7 +44,7 @@
     2.4  
     2.5  fun add_arity ((b, sorts, mx), sort) thy : theory =
     2.6    thy
     2.7 -  |> Sign.add_types [(b, length sorts, mx)]
     2.8 +  |> Sign.add_types_global [(b, length sorts, mx)]
     2.9    |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
    2.10  
    2.11  fun gen_add_domain
     3.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Apr 17 13:47:22 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Sun Apr 17 19:54:04 2011 +0200
     3.3 @@ -39,9 +39,9 @@
     3.4      val rep_bind = Binding.suffix_name "_rep" dbind
     3.5  
     3.6      val (abs_const, thy) =
     3.7 -        Sign.declare_const ((abs_bind, rhsT ->> lhsT), NoSyn) thy
     3.8 +        Sign.declare_const_global ((abs_bind, rhsT ->> lhsT), NoSyn) thy
     3.9      val (rep_const, thy) =
    3.10 -        Sign.declare_const ((rep_bind, lhsT ->> rhsT), NoSyn) thy
    3.11 +        Sign.declare_const_global ((rep_bind, lhsT ->> rhsT), NoSyn) thy
    3.12  
    3.13      val x = Free ("x", lhsT)
    3.14      val y = Free ("y", rhsT)
    3.15 @@ -98,7 +98,7 @@
    3.16      (* declare new types *)
    3.17      fun thy_type (dbind, mx, (lhsT, _)) =
    3.18          (dbind, (length o snd o dest_Type) lhsT, mx)
    3.19 -    val thy = Sign.add_types (map thy_type dom_eqns) thy
    3.20 +    val thy = Sign.add_types_global (map thy_type dom_eqns) thy
    3.21  
    3.22      (* axiomatize type constructor arities *)
    3.23      fun thy_arity (_, _, (lhsT, _)) =
     4.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 13:47:22 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Sun Apr 17 19:54:04 2011 +0200
     4.3 @@ -264,7 +264,7 @@
     4.4    val bisim_bind = Binding.suffix_name "_bisim" comp_dbind
     4.5    val bisim_type = R_types ---> boolT
     4.6    val (bisim_const, thy) =
     4.7 -      Sign.declare_const ((bisim_bind, bisim_type), NoSyn) thy
     4.8 +      Sign.declare_const_global ((bisim_bind, bisim_type), NoSyn) thy
     4.9  
    4.10    (* define bisimulation predicate *)
    4.11    local
     5.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 13:47:22 2011 +0200
     5.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 19:54:04 2011 +0200
     5.3 @@ -239,7 +239,7 @@
     5.4      : (term * thm) * theory =
     5.5    let
     5.6      val typ = Term.fastype_of rhs
     5.7 -    val (const, thy) = Sign.declare_const ((bind, typ), NoSyn) thy
     5.8 +    val (const, thy) = Sign.declare_const_global ((bind, typ), NoSyn) thy
     5.9      val eqn = Logic.mk_equals (const, rhs)
    5.10      val def = Thm.no_attributes (Binding.suffix_name "_def" bind, eqn)
    5.11      val (def_thm, thy) = yield_singleton (Global_Theory.add_defs false) def thy
    5.12 @@ -276,7 +276,7 @@
    5.13          val map_type = mapT lhsT
    5.14          val map_bind = Binding.suffix_name "_map" tbind
    5.15        in
    5.16 -        Sign.declare_const ((map_bind, map_type), NoSyn) thy
    5.17 +        Sign.declare_const_global ((map_bind, map_type), NoSyn) thy
    5.18        end
    5.19      val (map_consts, thy) = thy |>
    5.20        fold_map declare_map_const (dbinds ~~ dom_eqns)
    5.21 @@ -417,7 +417,7 @@
    5.22      (* this theory is used just for parsing *)
    5.23      val tmp_thy = thy |>
    5.24        Theory.copy |>
    5.25 -      Sign.add_types (map (fn (tvs, tbind, mx, _, morphs) =>
    5.26 +      Sign.add_types_global (map (fn (tvs, tbind, mx, _, morphs) =>
    5.27          (tbind, length tvs, mx)) doms_raw)
    5.28  
    5.29      fun prep_dom thy (vs, t, mx, typ_raw, morphs) sorts =
    5.30 @@ -499,7 +499,7 @@
    5.31          val defl_type =
    5.32            map Term.itselfT typeTs ---> map fastype_of defl_args -->> deflT
    5.33        in
    5.34 -        Sign.declare_const ((defl_bind, defl_type), NoSyn) thy
    5.35 +        Sign.declare_const_global ((defl_bind, defl_type), NoSyn) thy
    5.36        end
    5.37      val (defl_consts, thy) =
    5.38        fold_map declare_defl_const (defl_flagss ~~ doms) thy
     6.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Apr 17 13:47:22 2011 +0200
     6.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sun Apr 17 19:54:04 2011 +0200
     6.3 @@ -262,7 +262,7 @@
     6.4          val take_type = HOLogic.natT --> lhsT ->> lhsT
     6.5          val take_bind = Binding.suffix_name "_take" dbind
     6.6          val (take_const, thy) =
     6.7 -          Sign.declare_const ((take_bind, take_type), NoSyn) thy
     6.8 +          Sign.declare_const_global ((take_bind, take_type), NoSyn) thy
     6.9          val take_eqn = Logic.mk_equals (take_const, take_rhs)
    6.10          val (take_def_thm, thy) =
    6.11              add_qualified_def "take_def" (dbind, take_eqn) thy
    6.12 @@ -401,7 +401,7 @@
    6.13          val finite_type = lhsT --> boolT
    6.14          val finite_bind = Binding.suffix_name "_finite" dbind
    6.15          val (finite_const, thy) =
    6.16 -          Sign.declare_const ((finite_bind, finite_type), NoSyn) thy
    6.17 +          Sign.declare_const_global ((finite_bind, finite_type), NoSyn) thy
    6.18          val x = Free ("x", lhsT)
    6.19          val n = Free ("n", natT)
    6.20          val finite_rhs =
     7.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Apr 17 13:47:22 2011 +0200
     7.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Apr 17 19:54:04 2011 +0200
     7.3 @@ -194,7 +194,7 @@
     7.4  
     7.5      val tmp_thy = thy |>
     7.6        Theory.copy |>
     7.7 -      Sign.add_types (map (fn (tvs, tname, mx, _) =>
     7.8 +      Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
     7.9          (Binding.name tname, length tvs, mx)) dts);
    7.10  
    7.11      val atoms = atoms_of thy;
     8.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 13:47:22 2011 +0200
     8.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 19:54:04 2011 +0200
     8.3 @@ -649,7 +649,7 @@
     8.4      (* this theory is used just for parsing *)
     8.5      val tmp_thy = thy |>
     8.6        Theory.copy |>
     8.7 -      Sign.add_types (map (fn (tvs, tname, mx, _) =>
     8.8 +      Sign.add_types_global (map (fn (tvs, tname, mx, _) =>
     8.9          (tname, length tvs, mx)) dts);
    8.10  
    8.11      val (tyvars, _, _, _)::_ = dts;
     9.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Apr 17 13:47:22 2011 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Apr 17 19:54:04 2011 +0200
     9.3 @@ -321,7 +321,7 @@
     9.4                  fns2 @ (flat (drop (i + 1) case_dummy_fns)))));
     9.5            val ([def_thm], thy') =
     9.6              thy
     9.7 -            |> Sign.declare_const decl |> snd
     9.8 +            |> Sign.declare_const_global decl |> snd
     9.9              |> (Global_Theory.add_defs false o map Thm.no_attributes) [def];
    9.10  
    9.11          in (defs @ [def_thm], thy')
    10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 17 13:47:22 2011 +0200
    10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Apr 17 19:54:04 2011 +0200
    10.3 @@ -96,16 +96,16 @@
    10.4      val name_of = fst o dest_Const
    10.5      val thy = Proof_Context.theory_of ctxt |> Context.reject_draft
    10.6      val (maybe_t, thy) =
    10.7 -      Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    10.8 +      Sign.declare_const_global ((@{binding nitpick_maybe}, @{typ "'a => 'a"}),
    10.9                            Mixfix (maybe_mixfix (), [1000], 1000)) thy
   10.10      val (abs_t, thy) =
   10.11 -      Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
   10.12 +      Sign.declare_const_global ((@{binding nitpick_abs}, @{typ "'a => 'b"}),
   10.13                            Mixfix (abs_mixfix (), [40], 40)) thy
   10.14      val (base_t, thy) =
   10.15 -      Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}),
   10.16 +      Sign.declare_const_global ((@{binding nitpick_base}, @{typ "'a => 'a"}),
   10.17                            Mixfix (base_mixfix (), [1000], 1000)) thy
   10.18      val (step_t, thy) =
   10.19 -      Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}),
   10.20 +      Sign.declare_const_global ((@{binding nitpick_step}, @{typ "'a => 'a"}),
   10.21                            Mixfix (step_mixfix (), [1000], 1000)) thy
   10.22    in
   10.23      (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)),
    11.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Apr 17 13:47:22 2011 +0200
    11.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Apr 17 19:54:04 2011 +0200
    11.3 @@ -295,8 +295,9 @@
    11.4  
    11.5      val thy1' = thy1 |>
    11.6        Theory.copy |>
    11.7 -      Sign.add_types (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
    11.8 -        Extraction.add_typeof_eqns_i ty_eqs;
    11.9 +      Sign.add_types_global
   11.10 +        (map (fn s => (Binding.name (Long_Name.base_name s), ar, NoSyn)) tnames) |>
   11.11 +      Extraction.add_typeof_eqns_i ty_eqs;
   11.12      val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
   11.13        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
   11.14  
    12.1 --- a/src/HOL/Tools/record.ML	Sun Apr 17 13:47:22 2011 +0200
    12.2 +++ b/src/HOL/Tools/record.ML	Sun Apr 17 19:54:04 2011 +0200
    12.3 @@ -153,7 +153,7 @@
    12.4  
    12.5      val ([isom_def], cdef_thy) =
    12.6        typ_thy
    12.7 -      |> Sign.declare_const ((isom_binding, isomT), NoSyn) |> snd
    12.8 +      |> Sign.declare_const_global ((isom_binding, isomT), NoSyn) |> snd
    12.9        |> Global_Theory.add_defs false
   12.10          [((Binding.conceal (Thm.def_binding isom_binding), Logic.mk_equals (isom, body)), [])];
   12.11  
   12.12 @@ -1648,7 +1648,7 @@
   12.13  
   12.14      fun mk_defs () =
   12.15        typ_thy
   12.16 -      |> Sign.declare_const ((ext_binding, ext_type), NoSyn) |> snd
   12.17 +      |> Sign.declare_const_global ((ext_binding, ext_type), NoSyn) |> snd
   12.18        |> Global_Theory.add_defs false [((Thm.def_binding ext_binding, ext_spec), [])]
   12.19        ||> Theory.checkpoint
   12.20      val ([ext_def], defs_thy) =
   12.21 @@ -2087,9 +2087,9 @@
   12.22        |> Typedecl.abbrev_global
   12.23          (Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), NoSyn) rec_schemeT0 |> snd
   12.24        |> Sign.qualified_path false binding
   12.25 -      |> fold (fn ((x, T), mx) => snd o Sign.declare_const ((Binding.name x, T), mx))
   12.26 +      |> fold (fn ((x, T), mx) => snd o Sign.declare_const_global ((Binding.name x, T), mx))
   12.27          (sel_decls ~~ (field_syntax @ [NoSyn]))
   12.28 -      |> fold (fn (x, T) => snd o Sign.declare_const ((Binding.name x, T), NoSyn))
   12.29 +      |> fold (fn (x, T) => snd o Sign.declare_const_global ((Binding.name x, T), NoSyn))
   12.30          (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
   12.31        |> (Global_Theory.add_defs false o
   12.32              map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) sel_specs
    13.1 --- a/src/HOL/Tools/typedef.ML	Sun Apr 17 13:47:22 2011 +0200
    13.2 +++ b/src/HOL/Tools/typedef.ML	Sun Apr 17 19:54:04 2011 +0200
    13.3 @@ -92,7 +92,7 @@
    13.4          (newT --> oldT) --> (oldT --> newT) --> HOLogic.mk_setT oldT --> HOLogic.boolT);
    13.5    in Logic.mk_implies (mk_inhabited A, HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ A)) end;
    13.6  
    13.7 -fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A thy =
    13.8 +fun primitive_typedef typedef_name newT oldT Rep_name Abs_name A lthy =
    13.9    let
   13.10      (* errors *)
   13.11  
   13.12 @@ -111,18 +111,20 @@
   13.13  
   13.14      (* axiomatization *)
   13.15  
   13.16 -    val ((RepC, AbsC), consts_thy) = thy
   13.17 -      |> Sign.declare_const ((Rep_name, newT --> oldT), NoSyn)
   13.18 -      ||>> Sign.declare_const ((Abs_name, oldT --> newT), NoSyn);
   13.19 +    val ((RepC, AbsC), consts_lthy) = lthy
   13.20 +      |> Local_Theory.background_theory_result
   13.21 +        (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
   13.22 +          Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
   13.23  
   13.24      val typedef_deps = Term.add_consts A [];
   13.25  
   13.26 -    val ((axiom_name, axiom), axiom_thy) = consts_thy
   13.27 -      |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
   13.28 -      ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
   13.29 -      ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
   13.30 +    val ((axiom_name, axiom), axiom_lthy) = consts_lthy
   13.31 +      |> Local_Theory.background_theory_result
   13.32 +        (Thm.add_axiom consts_lthy (typedef_name, mk_typedef newT oldT RepC AbsC A) ##>
   13.33 +          Theory.add_deps consts_lthy "" (dest_Const RepC) typedef_deps ##>
   13.34 +          Theory.add_deps consts_lthy "" (dest_Const AbsC) typedef_deps);
   13.35  
   13.36 -  in ((RepC, AbsC, axiom_name, axiom), axiom_thy) end;
   13.37 +  in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
   13.38  
   13.39  
   13.40  (* prepare_typedef *)
   13.41 @@ -185,9 +187,8 @@
   13.42            Local_Defs.export_cterm set_lthy (Proof_Context.init_global thy) (cert set')
   13.43            ||> Thm.term_of;
   13.44  
   13.45 -        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy |>
   13.46 -          Local_Theory.background_theory_result
   13.47 -            (primitive_typedef typedef_name newT oldT Rep_name Abs_name A);
   13.48 +        val ((RepC, AbsC, axiom_name, axiom), axiom_lthy) = set_lthy
   13.49 +          |> primitive_typedef typedef_name newT oldT Rep_name Abs_name A;
   13.50  
   13.51          val cert = Thm.cterm_of (Proof_Context.theory_of axiom_lthy);
   13.52          val typedef =
    14.1 --- a/src/Pure/General/name_space.ML	Sun Apr 17 13:47:22 2011 +0200
    14.2 +++ b/src/Pure/General/name_space.ML	Sun Apr 17 19:54:04 2011 +0200
    14.3 @@ -46,10 +46,10 @@
    14.4    val qualified_path: bool -> binding -> naming -> naming
    14.5    val transform_binding: naming -> binding -> binding
    14.6    val full_name: naming -> binding -> string
    14.7 -  val declare: bool -> naming -> binding -> T -> string * T
    14.8 +  val declare: Proof.context -> bool -> naming -> binding -> T -> string * T
    14.9    val alias: naming -> binding -> string -> T -> T
   14.10    type 'a table = T * 'a Symtab.table
   14.11 -  val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   14.12 +  val define: Proof.context -> bool -> naming -> binding * 'a -> 'a table -> string * 'a table
   14.13    val empty_table: string -> 'a table
   14.14    val merge_tables: 'a table * 'a table -> 'a table
   14.15    val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
   14.16 @@ -335,7 +335,7 @@
   14.17              err_dup kind (dup, #2 (the (Symtab.lookup entries dup))) (name, entry);
   14.18      in (kind, internals, entries') end);
   14.19  
   14.20 -fun declare strict naming binding space =
   14.21 +fun declare ctxt strict naming binding space =
   14.22    let
   14.23      val Naming {group, theory_name, ...} = naming;
   14.24      val (concealed, spec) = name_spec naming binding;
   14.25 @@ -344,15 +344,17 @@
   14.26      val name = Long_Name.implode (map fst spec);
   14.27      val _ = name = "" andalso err_bad binding;
   14.28  
   14.29 +    val pos = Position.default (Binding.pos_of binding);
   14.30      val entry =
   14.31       {concealed = concealed,
   14.32        group = group,
   14.33        theory_name = theory_name,
   14.34 -      pos = Position.default (Binding.pos_of binding),
   14.35 +      pos = pos,
   14.36        id = serial ()};
   14.37      val space' = space
   14.38        |> fold (add_name name) accs
   14.39        |> new_entry strict (name, (accs', entry));
   14.40 +    val _ = Context_Position.report ctxt pos (entry_markup true (kind_of space) (name, entry));
   14.41    in (name, space') end;
   14.42  
   14.43  
   14.44 @@ -379,8 +381,8 @@
   14.45  
   14.46  type 'a table = T * 'a Symtab.table;
   14.47  
   14.48 -fun define strict naming (binding, x) (space, tab) =
   14.49 -  let val (name, space') = declare strict naming binding space
   14.50 +fun define ctxt strict naming (binding, x) (space, tab) =
   14.51 +  let val (name, space') = declare ctxt strict naming binding space
   14.52    in (name, (space', Symtab.update (name, x) tab)) end;
   14.53  
   14.54  fun empty_table kind = (empty kind, Symtab.empty);
    15.1 --- a/src/Pure/Isar/attrib.ML	Sun Apr 17 13:47:22 2011 +0200
    15.2 +++ b/src/Pure/Isar/attrib.ML	Sun Apr 17 19:54:04 2011 +0200
    15.3 @@ -83,7 +83,9 @@
    15.4    end;
    15.5  
    15.6  fun add_attribute name att comment thy = thy
    15.7 -  |> Attributes.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (att, comment)));
    15.8 +  |> Attributes.map
    15.9 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
   15.10 +      (name, (att, comment)) #> snd);
   15.11  
   15.12  
   15.13  (* name space *)
    16.1 --- a/src/Pure/Isar/class.ML	Sun Apr 17 13:47:22 2011 +0200
    16.2 +++ b/src/Pure/Isar/class.ML	Sun Apr 17 19:54:04 2011 +0200
    16.3 @@ -326,9 +326,9 @@
    16.4        |> map_types Type.strip_sorts;
    16.5    in
    16.6      thy
    16.7 -    |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
    16.8 +    |> Sign.declare_const_global ((b, Type.strip_sorts ty'), mx)
    16.9      |> snd
   16.10 -    |> Thm.add_def false false (b_def, def_eq)
   16.11 +    |> Thm.add_def_global false false (b_def, def_eq)
   16.12      |>> apsnd Thm.varifyT_global
   16.13      |-> (fn (_, def_thm) => Global_Theory.store_thm (b_def, def_thm)
   16.14        #> snd
    17.1 --- a/src/Pure/Isar/class_declaration.ML	Sun Apr 17 13:47:22 2011 +0200
    17.2 +++ b/src/Pure/Isar/class_declaration.ML	Sun Apr 17 19:54:04 2011 +0200
    17.3 @@ -253,7 +253,7 @@
    17.4          val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
    17.5        in
    17.6          thy
    17.7 -        |> Sign.declare_const ((b, ty0), syn)
    17.8 +        |> Sign.declare_const_global ((b, ty0), syn)
    17.9          |> snd
   17.10          |> pair ((Variable.name b, ty), (c, ty'))
   17.11        end;
    18.1 --- a/src/Pure/Isar/code.ML	Sun Apr 17 13:47:22 2011 +0200
    18.2 +++ b/src/Pure/Isar/code.ML	Sun Apr 17 19:54:04 2011 +0200
    18.3 @@ -339,21 +339,23 @@
    18.4  
    18.5  fun build_tsig thy =
    18.6    let
    18.7 -    val (tycos, _) = (the_signatures o the_exec) thy;
    18.8 -    val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy
    18.9 +    val ctxt = Syntax.init_pretty_global thy;
   18.10 +    val (tycos, _) = the_signatures (the_exec thy);
   18.11 +    val decls = #types (Type.rep_tsig (Sign.tsig_of thy))
   18.12        |> snd 
   18.13        |> Symtab.fold (fn (tyco, n) =>
   18.14            Symtab.update (tyco, Type.LogicalType n)) tycos;
   18.15    in
   18.16      Type.empty_tsig
   18.17 -    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type Name_Space.default_naming
   18.18 +    |> Symtab.fold (fn (tyco, Type.LogicalType n) => Type.add_type ctxt Name_Space.default_naming
   18.19          (Binding.qualified_name tyco, n) | _ => I) decls
   18.20    end;
   18.21  
   18.22 -fun cert_signature thy = Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
   18.23 +fun cert_signature thy =
   18.24 +  Logic.varifyT_global o Type.cert_typ (build_tsig thy) o Type.no_tvars;
   18.25  
   18.26 -fun read_signature thy = cert_signature thy o Type.strip_sorts
   18.27 -  o Syntax.parse_typ (Proof_Context.init_global thy);
   18.28 +fun read_signature thy =
   18.29 +  cert_signature thy o Type.strip_sorts o Syntax.parse_typ (Proof_Context.init_global thy);
   18.30  
   18.31  fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy);
   18.32  
    19.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 17 13:47:22 2011 +0200
    19.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 17 19:54:04 2011 +0200
    19.3 @@ -648,7 +648,7 @@
    19.4      val ([pred_def], defs_thy) =
    19.5        thy
    19.6        |> bodyT = propT ? Sign.add_advanced_trfuns ([], [], [aprop_tr' (length args) name], [])
    19.7 -      |> Sign.declare_const ((Binding.conceal binding, predT), NoSyn) |> snd
    19.8 +      |> Sign.declare_const_global ((Binding.conceal binding, predT), NoSyn) |> snd
    19.9        |> Global_Theory.add_defs false
   19.10          [((Binding.conceal (Thm.def_binding binding), Logic.mk_equals (head, body)), [])];
   19.11      val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head;
    20.1 --- a/src/Pure/Isar/generic_target.ML	Sun Apr 17 13:47:22 2011 +0200
    20.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Apr 17 19:54:04 2011 +0200
    20.3 @@ -198,11 +198,12 @@
    20.4  
    20.5  fun theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
    20.6    let
    20.7 -    val (const, lthy2) = lthy |> Local_Theory.background_theory_result
    20.8 -      (Sign.declare_const ((b, U), mx));
    20.9 +    val (const, lthy2) = lthy
   20.10 +      |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx));
   20.11      val lhs = list_comb (const, type_params @ term_params);
   20.12 -    val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result
   20.13 -      (Thm.add_def false false (b_def, Logic.mk_equals (lhs, rhs)));
   20.14 +    val ((_, def), lthy3) = lthy2
   20.15 +      |> Local_Theory.background_theory_result
   20.16 +        (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
   20.17    in ((lhs, def), lthy3) end;
   20.18  
   20.19  fun theory_notes kind global_facts lthy =
    21.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Apr 17 13:47:22 2011 +0200
    21.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Apr 17 19:54:04 2011 +0200
    21.3 @@ -129,7 +129,7 @@
    21.4  val _ =
    21.5    Outer_Syntax.command "nonterminal"
    21.6      "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
    21.7 -    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals));
    21.8 +    (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
    21.9  
   21.10  val _ =
   21.11    Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
    22.1 --- a/src/Pure/Isar/locale.ML	Sun Apr 17 13:47:22 2011 +0200
    22.2 +++ b/src/Pure/Isar/locale.ML	Sun Apr 17 19:54:04 2011 +0200
    22.3 @@ -173,7 +173,7 @@
    22.4    | NONE => error ("Unknown locale " ^ quote name));
    22.5  
    22.6  fun register_locale binding parameters spec intros axioms syntax_decls notes dependencies thy =
    22.7 -  thy |> Locales.map (Name_Space.define true (Sign.naming_of thy)
    22.8 +  thy |> Locales.map (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
    22.9      (binding,
   22.10        mk_locale ((parameters, spec, intros, axioms),
   22.11          ((map (fn decl => (decl, serial ())) syntax_decls, map (fn n => (n, serial ())) notes),
    23.1 --- a/src/Pure/Isar/method.ML	Sun Apr 17 13:47:22 2011 +0200
    23.2 +++ b/src/Pure/Isar/method.ML	Sun Apr 17 19:54:04 2011 +0200
    23.3 @@ -344,7 +344,9 @@
    23.4    end;
    23.5  
    23.6  fun add_method name meth comment thy = thy
    23.7 -  |> Methods.map (#2 o Name_Space.define true (Sign.naming_of thy) (name, (meth, comment)));
    23.8 +  |> Methods.map
    23.9 +    (Name_Space.define (Proof_Context.init_global thy) true (Sign.naming_of thy)
   23.10 +      (name, (meth, comment)) #> snd);
   23.11  
   23.12  
   23.13  (* get methods *)
    24.1 --- a/src/Pure/Isar/object_logic.ML	Sun Apr 17 13:47:22 2011 +0200
    24.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Apr 17 19:54:04 2011 +0200
    24.3 @@ -89,7 +89,7 @@
    24.4    let val c = Sign.full_name thy b in
    24.5      thy
    24.6      |> add_consts [(b, T, mx)]
    24.7 -    |> (fn thy' => Theory.add_deps c (c, Sign.the_const_type thy' c) [] thy')
    24.8 +    |> (fn thy' => Theory.add_deps_global c (c, Sign.the_const_type thy' c) [] thy')
    24.9      |> map_data (fn (base_sort, judgment, atomize_rulify) =>
   24.10          if is_some judgment then error "Attempt to redeclare object-logic judgment"
   24.11          else (base_sort, SOME c, atomize_rulify))
    25.1 --- a/src/Pure/Isar/overloading.ML	Sun Apr 17 13:47:22 2011 +0200
    25.2 +++ b/src/Pure/Isar/overloading.ML	Sun Apr 17 19:54:04 2011 +0200
    25.3 @@ -143,7 +143,8 @@
    25.4  
    25.5  fun define_overloaded (c, U) (v, checked) (b_def, rhs) =
    25.6    Local_Theory.background_theory_result
    25.7 -    (Thm.add_def (not checked) true (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
    25.8 +    (Thm.add_def_global (not checked) true
    25.9 +      (b_def, Logic.mk_equals (Const (c, Term.fastype_of rhs), rhs)))
   25.10    ##> map_overloading (filter_out (fn (_, (v', _)) => v' = v))
   25.11    ##> Local_Theory.target synchronize_syntax
   25.12    #-> (fn (_, def) => pair (Const (c, U), def))
    26.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 13:47:22 2011 +0200
    26.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 19:54:04 2011 +0200
    26.3 @@ -906,7 +906,7 @@
    26.4  
    26.5  fun update_thms _ (b, NONE) ctxt = ctxt |> map_facts (Facts.del (full_name ctxt b))
    26.6    | update_thms do_props (b, SOME ths) ctxt = ctxt |> map_facts
    26.7 -      (Facts.add_local do_props (naming_of ctxt) (b, ths) #> snd);
    26.8 +      (Facts.add_local ctxt do_props (naming_of ctxt) (b, ths) #> snd);
    26.9  
   26.10  in
   26.11  
   26.12 @@ -1033,7 +1033,7 @@
   26.13        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
   26.14      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   26.15      val ((lhs, rhs), consts') = consts_of ctxt
   26.16 -      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode (b, t);
   26.17 +      |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
   26.18    in
   26.19      ctxt
   26.20      |> (map_consts o apfst) (K consts')
    27.1 --- a/src/Pure/Isar/specification.ML	Sun Apr 17 13:47:22 2011 +0200
    27.2 +++ b/src/Pure/Isar/specification.ML	Sun Apr 17 19:54:04 2011 +0200
    27.3 @@ -180,7 +180,7 @@
    27.4  
    27.5      (*axioms*)
    27.6      val (axioms, axioms_thy) = (specs, consts_thy) |-> fold_map (fn ((b, atts), props) =>
    27.7 -        fold_map Thm.add_axiom
    27.8 +        fold_map Thm.add_axiom_global
    27.9            (map (apfst (fn a => Binding.map_name (K a) b))
   27.10              (Global_Theory.name_multi (Variable.name b) (map subst props)))
   27.11          #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
    28.1 --- a/src/Pure/Isar/typedecl.ML	Sun Apr 17 13:47:22 2011 +0200
    28.2 +++ b/src/Pure/Isar/typedecl.ML	Sun Apr 17 19:54:04 2011 +0200
    28.3 @@ -40,8 +40,9 @@
    28.4      |> pair name
    28.5    end;
    28.6  
    28.7 -fun basic_typedecl (b, n, mx) =
    28.8 -  basic_decl (fn name => Sign.add_types [(b, n, NoSyn)] #> object_logic_arity name) (b, n, mx);
    28.9 +fun basic_typedecl (b, n, mx) lthy =
   28.10 +  basic_decl (fn name => Sign.add_types lthy [(b, n, NoSyn)] #> object_logic_arity name)
   28.11 +    (b, n, mx) lthy;
   28.12  
   28.13  
   28.14  (* global type -- without dependencies on type parameters of the context *)
   28.15 @@ -91,7 +92,7 @@
   28.16        handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   28.17    in
   28.18      lthy
   28.19 -    |> basic_decl (fn _ => Sign.add_type_abbrev (b, vs, rhs)) (b, length vs, mx)
   28.20 +    |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
   28.21      |> snd
   28.22      |> pair name
   28.23    end;
    29.1 --- a/src/Pure/Proof/extraction.ML	Sun Apr 17 13:47:22 2011 +0200
    29.2 +++ b/src/Pure/Proof/extraction.ML	Sun Apr 17 19:54:04 2011 +0200
    29.3 @@ -36,7 +36,7 @@
    29.4    thy
    29.5    |> Theory.copy
    29.6    |> Sign.root_path
    29.7 -  |> Sign.add_types [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    29.8 +  |> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
    29.9    |> Sign.add_consts
   29.10        [(Binding.name "typeof", "'b::{} => Type", NoSyn),
   29.11         (Binding.name "Type", "'a::{} itself => Type", NoSyn),
    30.1 --- a/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 13:47:22 2011 +0200
    30.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Apr 17 19:54:04 2011 +0200
    30.3 @@ -45,8 +45,8 @@
    30.4    |> Theory.copy
    30.5    |> Sign.root_path
    30.6    |> Sign.set_defsort []
    30.7 -  |> Sign.add_types [(Binding.name "proof", 0, NoSyn)]
    30.8 -  |> fold (snd oo Sign.declare_const)
    30.9 +  |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
   30.10 +  |> fold (snd oo Sign.declare_const_global)
   30.11        [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
   30.12         ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
   30.13         ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
   30.14 @@ -55,7 +55,7 @@
   30.15         ((Binding.name "Oracle", propT --> proofT), NoSyn),
   30.16         ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
   30.17         ((Binding.name "MinProof", proofT), Delimfix "?")]
   30.18 -  |> Sign.add_nonterminals [Binding.name "param", Binding.name "params"]
   30.19 +  |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
   30.20    |> Sign.add_syntax_i
   30.21        [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
   30.22         ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
    31.1 --- a/src/Pure/axclass.ML	Sun Apr 17 13:47:22 2011 +0200
    31.2 +++ b/src/Pure/axclass.ML	Sun Apr 17 19:54:04 2011 +0200
    31.3 @@ -384,9 +384,9 @@
    31.4    in
    31.5      thy
    31.6      |> Sign.qualified_path true (Binding.name name_inst)
    31.7 -    |> Sign.declare_const ((Binding.name c', T'), NoSyn)
    31.8 +    |> Sign.declare_const_global ((Binding.name c', T'), NoSyn)
    31.9      |-> (fn const' as Const (c'', _) =>
   31.10 -      Thm.add_def false true
   31.11 +      Thm.add_def_global false true
   31.12          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
   31.13        #>> apsnd Thm.varifyT_global
   31.14        #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
   31.15 @@ -405,7 +405,7 @@
   31.16      val b' = Thm.def_binding_optional (Binding.name (instance_name (tyco, c))) b;
   31.17    in
   31.18      thy
   31.19 -    |> Thm.add_def false false (b', prop)
   31.20 +    |> Thm.add_def_global false false (b', prop)
   31.21      |>> (fn (_, thm) => Drule.transitive_thm OF [eq, thm])
   31.22    end;
   31.23  
   31.24 @@ -608,7 +608,7 @@
   31.25      val names = name args;
   31.26    in
   31.27      thy
   31.28 -    |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
   31.29 +    |> fold_map Thm.add_axiom_global (map Binding.name names ~~ specs)
   31.30      |-> fold (add o Drule.export_without_context o snd)
   31.31    end;
   31.32  
   31.33 @@ -631,13 +631,14 @@
   31.34      thy
   31.35      |> Sign.primitive_class (bclass, super)
   31.36      |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
   31.37 -    |> Theory.add_deps "" (class_const class) (map class_const super)
   31.38 +    |> Theory.add_deps_global "" (class_const class) (map class_const super)
   31.39    end;
   31.40  
   31.41  in
   31.42  
   31.43  val axiomatize_class = ax_class Sign.certify_class cert_classrel;
   31.44 -val axiomatize_class_cmd = ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
   31.45 +val axiomatize_class_cmd =
   31.46 +  ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
   31.47  val axiomatize_classrel = ax_classrel cert_classrel;
   31.48  val axiomatize_classrel_cmd = ax_classrel read_classrel;
   31.49  val axiomatize_arity = ax_arity Proof_Context.cert_arity;
    32.1 --- a/src/Pure/consts.ML	Sun Apr 17 13:47:22 2011 +0200
    32.2 +++ b/src/Pure/consts.ML	Sun Apr 17 19:54:04 2011 +0200
    32.3 @@ -29,9 +29,9 @@
    32.4    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
    32.5    val typargs: T -> string * typ -> typ list
    32.6    val instance: T -> string * typ list -> typ
    32.7 -  val declare: Name_Space.naming -> binding * typ -> T -> T
    32.8 +  val declare: Proof.context -> Name_Space.naming -> binding * typ -> T -> T
    32.9    val constrain: string * typ option -> T -> T
   32.10 -  val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string ->
   32.11 +  val abbreviate: Proof.context -> Type.tsig -> Name_Space.naming -> string ->
   32.12      binding * term -> T -> (term * term) * T
   32.13    val revert_abbrev: string -> string -> T -> T
   32.14    val hide: bool -> string -> T -> T
   32.15 @@ -231,12 +231,12 @@
   32.16  
   32.17  (* declarations *)
   32.18  
   32.19 -fun declare naming (b, declT) =
   32.20 +fun declare ctxt naming (b, declT) =
   32.21    map_consts (fn (decls, constraints, rev_abbrevs) =>
   32.22      let
   32.23        val decl = {T = declT, typargs = typargs_of declT};
   32.24        val _ = Binding.check b;
   32.25 -      val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
   32.26 +      val (_, decls') = decls |> Name_Space.define ctxt true naming (b, (decl, NONE));
   32.27      in (decls', constraints, rev_abbrevs) end);
   32.28  
   32.29  
   32.30 @@ -267,8 +267,9 @@
   32.31  
   32.32  in
   32.33  
   32.34 -fun abbreviate pp tsig naming mode (b, raw_rhs) consts =
   32.35 +fun abbreviate ctxt tsig naming mode (b, raw_rhs) consts =
   32.36    let
   32.37 +    val pp = Syntax.pp ctxt;
   32.38      val cert_term = certify pp tsig false consts;
   32.39      val expand_term = certify pp tsig true consts;
   32.40      val force_expand = mode = Print_Mode.internal;
   32.41 @@ -290,7 +291,7 @@
   32.42          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
   32.43          val _ = Binding.check b;
   32.44          val (_, decls') = decls
   32.45 -          |> Name_Space.define true naming (b, (decl, SOME abbr));
   32.46 +          |> Name_Space.define ctxt true naming (b, (decl, SOME abbr));
   32.47          val rev_abbrevs' = rev_abbrevs
   32.48            |> update_abbrevs mode (rev_abbrev lhs rhs);
   32.49        in (decls', constraints, rev_abbrevs') end)
    33.1 --- a/src/Pure/facts.ML	Sun Apr 17 13:47:22 2011 +0200
    33.2 +++ b/src/Pure/facts.ML	Sun Apr 17 19:54:04 2011 +0200
    33.3 @@ -32,9 +32,10 @@
    33.4    val props: T -> thm list
    33.5    val could_unify: T -> term -> thm list
    33.6    val merge: T * T -> T
    33.7 -  val add_global: Name_Space.naming -> binding * thm list -> T -> string * T
    33.8 -  val add_local: bool -> Name_Space.naming -> binding * thm list -> T -> string * T
    33.9 -  val add_dynamic: Name_Space.naming -> binding * (Context.generic -> thm list) -> T -> string * T
   33.10 +  val add_global: Proof.context -> Name_Space.naming -> binding * thm list -> T -> string * T
   33.11 +  val add_local: Proof.context -> bool -> Name_Space.naming -> binding * thm list -> T -> string * T
   33.12 +  val add_dynamic: Proof.context -> Name_Space.naming ->
   33.13 +    binding * (Context.generic -> thm list) -> T -> string * T
   33.14    val del: string -> T -> T
   33.15    val hide: bool -> string -> T -> T
   33.16  end;
   33.17 @@ -190,11 +191,11 @@
   33.18  
   33.19  local
   33.20  
   33.21 -fun add strict do_props naming (b, ths) (Facts {facts, props}) =
   33.22 +fun add ctxt strict do_props naming (b, ths) (Facts {facts, props}) =
   33.23    let
   33.24      val (name, facts') =
   33.25        if Binding.is_empty b then ("", facts)
   33.26 -      else Name_Space.define strict naming (b, Static ths) facts;
   33.27 +      else Name_Space.define ctxt strict naming (b, Static ths) facts;
   33.28      val props' =
   33.29        if do_props
   33.30        then fold (fn th => Net.insert_term (K false) (Thm.full_prop_of th, th)) ths props
   33.31 @@ -203,16 +204,16 @@
   33.32  
   33.33  in
   33.34  
   33.35 -val add_global = add true false;
   33.36 -val add_local = add false;
   33.37 +fun add_global ctxt = add ctxt true false;
   33.38 +fun add_local ctxt = add ctxt false;
   33.39  
   33.40  end;
   33.41  
   33.42  
   33.43  (* add dynamic entries *)
   33.44  
   33.45 -fun add_dynamic naming (b, f) (Facts {facts, props}) =
   33.46 -  let val (name, facts') = Name_Space.define true naming (b, Dynamic f) facts;
   33.47 +fun add_dynamic ctxt naming (b, f) (Facts {facts, props}) =
   33.48 +  let val (name, facts') = Name_Space.define ctxt true naming (b, Dynamic f) facts;
   33.49    in (name, make_facts facts' props) end;
   33.50  
   33.51  
    34.1 --- a/src/Pure/global_theory.ML	Sun Apr 17 13:47:22 2011 +0200
    34.2 +++ b/src/Pure/global_theory.ML	Sun Apr 17 19:54:04 2011 +0200
    34.3 @@ -140,7 +140,9 @@
    34.4        val (thy', thms') =
    34.5          register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
    34.6        val thms'' = map (Thm.transfer thy') thms';
    34.7 -      val thy'' = thy' |> (Data.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
    34.8 +      val thy'' = thy'
    34.9 +        |> (Data.map o apfst)
   34.10 +            (Facts.add_global (Proof_Context.init_global thy') naming (b, thms'') #> snd);
   34.11      in (thms'', thy'') end;
   34.12  
   34.13  
   34.14 @@ -176,7 +178,7 @@
   34.15  
   34.16  fun add_thms_dynamic (b, f) thy = thy
   34.17    |> (Data.map o apfst)
   34.18 -      (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
   34.19 +      (Facts.add_dynamic (Proof_Context.init_global thy) (Sign.naming_of thy) (b, f) #> snd);
   34.20  
   34.21  
   34.22  (* note_thmss *)
   34.23 @@ -200,14 +202,15 @@
   34.24  
   34.25  fun no_read _ (_, t) = t;
   34.26  
   34.27 -fun read thy (b, str) =
   34.28 -  Syntax.read_prop_global thy str handle ERROR msg =>
   34.29 +fun read ctxt (b, str) =
   34.30 +  Syntax.read_prop ctxt str handle ERROR msg =>
   34.31      cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
   34.32  
   34.33  fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   34.34    let
   34.35 -    val prop = prep thy (b, raw_prop);
   34.36 -    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
   34.37 +    val ctxt = Syntax.init_pretty_global thy;
   34.38 +    val prop = prep ctxt (b, raw_prop);
   34.39 +    val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
   34.40      val thm = def
   34.41        |> Thm.forall_intr_frees
   34.42        |> Thm.forall_elim_vars 0
    35.1 --- a/src/Pure/more_thm.ML	Sun Apr 17 13:47:22 2011 +0200
    35.2 +++ b/src/Pure/more_thm.ML	Sun Apr 17 19:54:04 2011 +0200
    35.3 @@ -63,8 +63,10 @@
    35.4    val forall_intr_frees: thm -> thm
    35.5    val unvarify_global: thm -> thm
    35.6    val close_derivation: thm -> thm
    35.7 -  val add_axiom: binding * term -> theory -> (string * thm) * theory
    35.8 -  val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
    35.9 +  val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
   35.10 +  val add_axiom_global: binding * term -> theory -> (string * thm) * theory
   35.11 +  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
   35.12 +  val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   35.13    type attribute = Context.generic * thm -> Context.generic * thm
   35.14    type binding = binding * attribute list
   35.15    val empty_binding: binding
   35.16 @@ -346,17 +348,17 @@
   35.17      val t' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip))) t;
   35.18    in (strip, recover, t') end;
   35.19  
   35.20 -fun add_axiom (b, prop) thy =
   35.21 +fun add_axiom ctxt (b, prop) thy =
   35.22    let
   35.23      val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
   35.24  
   35.25 -    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
   35.26 +    val _ = Sign.no_vars ctxt prop;
   35.27      val (strip, recover, prop') = stripped_sorts thy prop;
   35.28      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
   35.29      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
   35.30  
   35.31 -    val thy' =
   35.32 -      Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
   35.33 +    val thy' = thy
   35.34 +      |> Theory.add_axiom ctxt (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop'));
   35.35      val axm_name = Sign.full_name thy' b';
   35.36      val axm' = Thm.axiom thy' axm_name;
   35.37      val thm =
   35.38 @@ -365,13 +367,15 @@
   35.39        |> fold elim_implies of_sorts;
   35.40    in ((axm_name, thm), thy') end;
   35.41  
   35.42 -fun add_def unchecked overloaded (b, prop) thy =
   35.43 +fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
   35.44 +
   35.45 +fun add_def ctxt unchecked overloaded (b, prop) thy =
   35.46    let
   35.47 -    val _ = Sign.no_vars (Syntax.init_pretty_global thy) prop;
   35.48 +    val _ = Sign.no_vars ctxt prop;
   35.49      val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
   35.50      val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
   35.51  
   35.52 -    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
   35.53 +    val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
   35.54      val axm_name = Sign.full_name thy' b;
   35.55      val axm' = Thm.axiom thy' axm_name;
   35.56      val thm =
   35.57 @@ -380,6 +384,9 @@
   35.58        |> fold_rev Thm.implies_intr prems;
   35.59    in ((axm_name, thm), thy') end;
   35.60  
   35.61 +fun add_def_global unchecked overloaded arg thy =
   35.62 +  add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy;
   35.63 +
   35.64  
   35.65  
   35.66  (** attributes **)
    36.1 --- a/src/Pure/pure_thy.ML	Sun Apr 17 13:47:22 2011 +0200
    36.2 +++ b/src/Pure/pure_thy.ML	Sun Apr 17 19:54:04 2011 +0200
    36.3 @@ -55,12 +55,12 @@
    36.4  val _ = Context.>> (Context.map_theory
    36.5    (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
    36.6     Old_Appl_Syntax.put false #>
    36.7 -   Sign.add_types
    36.8 +   Sign.add_types_global
    36.9     [(Binding.name "fun", 2, NoSyn),
   36.10      (Binding.name "prop", 0, NoSyn),
   36.11      (Binding.name "itself", 1, NoSyn),
   36.12      (Binding.name "dummy", 0, NoSyn)]
   36.13 -  #> Sign.add_nonterminals (map Binding.name Syntax.basic_nonterms)
   36.14 +  #> Sign.add_nonterminals_global (map Binding.name Syntax.basic_nonterms)
   36.15    #> Sign.add_syntax_i (map (fn x => (x, typ "'a", NoSyn)) Syntax.token_markers)
   36.16    #> Sign.add_syntax_i
   36.17     [("",            typ "prop' => prop",               Delimfix "_"),
   36.18 @@ -177,11 +177,11 @@
   36.19      (Binding.name "prop", typ "prop => prop", NoSyn),
   36.20      (Binding.name "TYPE", typ "'a itself", NoSyn),
   36.21      (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
   36.22 -  #> Theory.add_deps "==" ("==", typ "'a => 'a => prop") []
   36.23 -  #> Theory.add_deps "==>" ("==>", typ "prop => prop => prop") []
   36.24 -  #> Theory.add_deps "all" ("all", typ "('a => prop) => prop") []
   36.25 -  #> Theory.add_deps "TYPE" ("TYPE", typ "'a itself") []
   36.26 -  #> Theory.add_deps Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   36.27 +  #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
   36.28 +  #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
   36.29 +  #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
   36.30 +  #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
   36.31 +  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
   36.32    #> Sign.add_trfuns Syntax_Trans.pure_trfuns
   36.33    #> Sign.local_path
   36.34    #> Sign.add_consts_i
   36.35 @@ -199,6 +199,7 @@
   36.36    #> Sign.hide_const false "Pure.sort_constraint"
   36.37    #> Sign.hide_const false "Pure.conjunction"
   36.38    #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
   36.39 -  #> fold (fn (a, prop) => snd o Thm.add_axiom (Binding.name a, prop)) Proofterm.equality_axms));
   36.40 +  #> fold (fn (a, prop) =>
   36.41 +      snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms));
   36.42  
   36.43  end;
    37.1 --- a/src/Pure/sign.ML	Sun Apr 17 13:47:22 2011 +0200
    37.2 +++ b/src/Pure/sign.ML	Sun Apr 17 19:54:04 2011 +0200
    37.3 @@ -67,9 +67,11 @@
    37.4    val cert_prop: theory -> term -> term
    37.5    val no_frees: Proof.context -> term -> term
    37.6    val no_vars: Proof.context -> term -> term
    37.7 -  val add_types: (binding * int * mixfix) list -> theory -> theory
    37.8 -  val add_nonterminals: binding list -> theory -> theory
    37.9 -  val add_type_abbrev: binding * string list * typ -> theory -> theory
   37.10 +  val add_types: Proof.context -> (binding * int * mixfix) list -> theory -> theory
   37.11 +  val add_types_global: (binding * int * mixfix) list -> theory -> theory
   37.12 +  val add_nonterminals: Proof.context -> binding list -> theory -> theory
   37.13 +  val add_nonterminals_global: binding list -> theory -> theory
   37.14 +  val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
   37.15    val add_syntax: (string * string * mixfix) list -> theory -> theory
   37.16    val add_syntax_i: (string * typ * mixfix) list -> theory -> theory
   37.17    val add_modesyntax: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   37.18 @@ -78,7 +80,8 @@
   37.19    val del_modesyntax_i: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   37.20    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   37.21    val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   37.22 -  val declare_const: (binding * typ) * mixfix -> theory -> term * theory
   37.23 +  val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
   37.24 +  val declare_const_global: (binding * typ) * mixfix -> theory -> term * theory
   37.25    val add_consts: (binding * string * mixfix) list -> theory -> theory
   37.26    val add_consts_i: (binding * typ * mixfix) list -> theory -> theory
   37.27    val add_abbrev: string -> binding * term -> theory -> (term * term) * theory
   37.28 @@ -325,25 +328,31 @@
   37.29  
   37.30  (* add type constructors *)
   37.31  
   37.32 -fun add_types types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   37.33 +fun add_types ctxt types thy = thy |> map_sign (fn (naming, syn, tsig, consts) =>
   37.34    let
   37.35      fun type_syntax (b, n, mx) =
   37.36        (Lexicon.mark_type (Name_Space.full_name naming b), Mixfix.make_type n, mx);
   37.37      val syn' = Syntax.update_type_gram true Syntax.mode_default (map type_syntax types) syn;
   37.38 -    val tsig' = fold (fn (a, n, _) => Type.add_type naming (a, n)) types tsig;
   37.39 +    val tsig' = fold (fn (a, n, _) => Type.add_type ctxt naming (a, n)) types tsig;
   37.40    in (naming, syn', tsig', consts) end);
   37.41  
   37.42 +fun add_types_global types thy =
   37.43 +  add_types (Syntax.init_pretty_global thy) types thy;
   37.44 +
   37.45  
   37.46  (* add nonterminals *)
   37.47  
   37.48 -fun add_nonterminals ns = map_sign (fn (naming, syn, tsig, consts) =>
   37.49 -  (naming, syn, fold (Type.add_nonterminal naming) ns tsig, consts));
   37.50 +fun add_nonterminals ctxt ns = map_sign (fn (naming, syn, tsig, consts) =>
   37.51 +  (naming, syn, fold (Type.add_nonterminal ctxt naming) ns tsig, consts));
   37.52 +
   37.53 +fun add_nonterminals_global ns thy =
   37.54 +  add_nonterminals (Syntax.init_pretty_global thy) ns thy;
   37.55  
   37.56  
   37.57  (* add type abbreviations *)
   37.58  
   37.59 -fun add_type_abbrev abbr = map_sign (fn (naming, syn, tsig, consts) =>
   37.60 -  (naming, syn, Type.add_abbrev naming abbr tsig, consts));
   37.61 +fun add_type_abbrev ctxt abbr = map_sign (fn (naming, syn, tsig, consts) =>
   37.62 +  (naming, syn, Type.add_abbrev ctxt naming abbr tsig, consts));
   37.63  
   37.64  
   37.65  (* modify syntax *)
   37.66 @@ -385,9 +394,8 @@
   37.67  
   37.68  local
   37.69  
   37.70 -fun gen_add_consts parse_typ raw_args thy =
   37.71 +fun gen_add_consts parse_typ ctxt raw_args thy =
   37.72    let
   37.73 -    val ctxt = Proof_Context.init_global thy;
   37.74      val prepT = Type.no_tvars o Term.no_dummyT o certify_typ thy o parse_typ ctxt;
   37.75      fun prep (b, raw_T, mx) =
   37.76        let
   37.77 @@ -399,23 +407,27 @@
   37.78      val args = map prep raw_args;
   37.79    in
   37.80      thy
   37.81 -    |> map_consts (fold (Consts.declare (naming_of thy) o #1) args)
   37.82 +    |> map_consts (fold (Consts.declare ctxt (naming_of thy) o #1) args)
   37.83      |> add_syntax_i (map #2 args)
   37.84      |> pair (map #3 args)
   37.85    end;
   37.86  
   37.87  in
   37.88  
   37.89 -fun add_consts args = snd o gen_add_consts Syntax.parse_typ args;
   37.90 -fun add_consts_i args = snd o gen_add_consts (K I) args;
   37.91 +fun add_consts args thy =
   37.92 +  #2 (gen_add_consts Syntax.parse_typ (Proof_Context.init_global thy) args thy);
   37.93 +fun add_consts_i args thy =
   37.94 +  #2 (gen_add_consts (K I) (Proof_Context.init_global thy) args thy);
   37.95  
   37.96 -fun declare_const ((b, T), mx) thy =
   37.97 +fun declare_const ctxt ((b, T), mx) thy =
   37.98    let
   37.99      val pos = Binding.pos_of b;
  37.100 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) [(b, T, mx)] thy;
  37.101 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) ctxt [(b, T, mx)] thy;
  37.102      val _ = Position.report pos (Markup.const_decl c);
  37.103    in (const, thy') end;
  37.104  
  37.105 +fun declare_const_global arg thy = declare_const (Proof_Context.init_global thy) arg thy;
  37.106 +
  37.107  end;
  37.108  
  37.109  
  37.110 @@ -428,7 +440,7 @@
  37.111      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
  37.112        handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
  37.113      val (res, consts') = consts_of thy
  37.114 -      |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of thy) (naming_of thy) mode (b, t);
  37.115 +      |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
  37.116    in (res, thy |> map_consts (K consts')) end;
  37.117  
  37.118  fun revert_abbrev mode c = map_consts (Consts.revert_abbrev mode c);
  37.119 @@ -450,7 +462,8 @@
  37.120  fun primitive_class (bclass, classes) thy =
  37.121    thy |> map_sign (fn (naming, syn, tsig, consts) =>
  37.122      let
  37.123 -      val tsig' = Type.add_class (Syntax.pp_global thy) naming (bclass, classes) tsig;
  37.124 +      val ctxt = Syntax.init_pretty_global thy;
  37.125 +      val tsig' = Type.add_class ctxt (Syntax.pp ctxt) naming (bclass, classes) tsig;
  37.126      in (naming, syn, tsig', consts) end)
  37.127    |> add_consts_i [(Binding.map_name Logic.const_of_class bclass, Term.a_itselfT --> propT, NoSyn)];
  37.128  
    38.1 --- a/src/Pure/simplifier.ML	Sun Apr 17 13:47:22 2011 +0200
    38.2 +++ b/src/Pure/simplifier.ML	Sun Apr 17 19:54:04 2011 +0200
    38.3 @@ -197,13 +197,15 @@
    38.4         proc = proc,
    38.5         identifier = identifier};
    38.6    in
    38.7 -    lthy |> Local_Theory.declaration false (fn phi =>
    38.8 +    lthy |> Local_Theory.declaration false (fn phi => fn context =>
    38.9        let
   38.10          val b' = Morphism.binding phi b;
   38.11          val simproc' = morph_simproc phi simproc;
   38.12        in
   38.13 -        Simprocs.map (#2 o Name_Space.define true naming (b', simproc'))
   38.14 -        #> map_ss (fn ss => ss addsimprocs [simproc'])
   38.15 +        context
   38.16 +        |> Simprocs.map
   38.17 +          (#2 o Name_Space.define (Context.proof_of context) true naming (b', simproc'))
   38.18 +        |> map_ss (fn ss => ss addsimprocs [simproc'])
   38.19        end)
   38.20    end;
   38.21  
    39.1 --- a/src/Pure/theory.ML	Sun Apr 17 13:47:22 2011 +0200
    39.2 +++ b/src/Pure/theory.ML	Sun Apr 17 19:54:04 2011 +0200
    39.3 @@ -28,9 +28,10 @@
    39.4    val at_end: (theory -> theory option) -> theory -> theory
    39.5    val begin_theory: string -> theory list -> theory
    39.6    val end_theory: theory -> theory
    39.7 -  val add_axiom: binding * term -> theory -> theory
    39.8 -  val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
    39.9 -  val add_def: bool -> bool -> binding * term -> theory -> theory
   39.10 +  val add_axiom: Proof.context -> binding * term -> theory -> theory
   39.11 +  val add_deps: Proof.context -> string -> string * typ -> (string * typ) list -> theory -> theory
   39.12 +  val add_deps_global: string -> string * typ -> (string * typ) list -> theory -> theory
   39.13 +  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
   39.14    val add_finals_i: bool -> term list -> theory -> theory
   39.15    val add_finals: bool -> string list -> theory -> theory
   39.16    val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   39.17 @@ -154,37 +155,35 @@
   39.18  
   39.19  (* raw axioms *)
   39.20  
   39.21 -fun cert_axm thy (b, raw_tm) =
   39.22 +fun cert_axm ctxt (b, raw_tm) =
   39.23    let
   39.24 +    val thy = Proof_Context.theory_of ctxt;
   39.25      val t = Sign.cert_prop thy raw_tm
   39.26        handle TYPE (msg, _, _) => error msg
   39.27          | TERM (msg, _) => error msg;
   39.28      val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
   39.29  
   39.30 -    val ctxt = Syntax.init_pretty_global thy
   39.31 -      |> Config.put show_sorts true;
   39.32      val bad_sorts =
   39.33        rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
   39.34      val _ = null bad_sorts orelse
   39.35        error ("Illegal sort constraints in primitive specification: " ^
   39.36 -        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
   39.37 -  in
   39.38 -    (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   39.39 -  end handle ERROR msg =>
   39.40 +        commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
   39.41 +  in (b, Sign.no_vars ctxt t) end
   39.42 +  handle ERROR msg =>
   39.43      cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
   39.44  
   39.45 -fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
   39.46 +fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   39.47    let
   39.48 -    val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
   39.49 -    val (_, axioms') = Name_Space.define true (Sign.naming_of thy) axm axioms;
   39.50 +    val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm);
   39.51 +    val (_, axioms') = Name_Space.define ctxt true (Sign.naming_of thy) axm axioms;
   39.52    in axioms' end);
   39.53  
   39.54  
   39.55  (* dependencies *)
   39.56  
   39.57 -fun dependencies thy unchecked def description lhs rhs =
   39.58 +fun dependencies ctxt unchecked def description lhs rhs =
   39.59    let
   39.60 -    val ctxt = Syntax.init_pretty_global thy;
   39.61 +    val thy = Proof_Context.theory_of ctxt;
   39.62      val consts = Sign.consts_of thy;
   39.63      fun prep const =
   39.64        let val Const (c, T) = Sign.no_vars ctxt (Const const)
   39.65 @@ -200,26 +199,29 @@
   39.66          "\nThe error(s) above occurred in " ^ quote description);
   39.67    in Defs.define (Syntax.pp ctxt) unchecked def description (prep lhs) (map prep rhs) end;
   39.68  
   39.69 -fun add_deps a raw_lhs raw_rhs thy =
   39.70 +fun add_deps ctxt a raw_lhs raw_rhs thy =
   39.71    let
   39.72      val lhs :: rhs = map (dest_Const o Sign.cert_term thy o Const) (raw_lhs :: raw_rhs);
   39.73      val description = if a = "" then #1 lhs ^ " axiom" else a;
   39.74 -  in thy |> map_defs (dependencies thy false NONE description lhs rhs) end;
   39.75 +  in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
   39.76 +
   39.77 +fun add_deps_global a x y thy = add_deps (Syntax.init_pretty_global thy) a x y thy;
   39.78  
   39.79  fun specify_const decl thy =
   39.80 -  let val (t as Const const, thy') = Sign.declare_const decl thy
   39.81 -  in (t, add_deps "" const [] thy') end;
   39.82 +  let val (t as Const const, thy') = Sign.declare_const_global decl thy;
   39.83 +  in (t, add_deps_global "" const [] thy') end;
   39.84  
   39.85  
   39.86  (* overloading *)
   39.87  
   39.88 -fun check_overloading thy overloaded (c, T) =
   39.89 +fun check_overloading ctxt overloaded (c, T) =
   39.90    let
   39.91 +    val thy = Proof_Context.theory_of ctxt;
   39.92 +
   39.93      val declT = Sign.the_const_constraint thy c
   39.94        handle TYPE (msg, _, _) => error msg;
   39.95      val T' = Logic.varifyT_global T;
   39.96  
   39.97 -    val ctxt = Syntax.init_pretty_global thy;
   39.98      fun message sorts txt =
   39.99        [Pretty.block [Pretty.str "Specification of constant ",
  39.100          Pretty.str c, Pretty.str " ::", Pretty.brk 1,
  39.101 @@ -238,27 +240,27 @@
  39.102  
  39.103  local
  39.104  
  39.105 -fun check_def thy unchecked overloaded (b, tm) defs =
  39.106 +fun check_def ctxt unchecked overloaded (b, tm) defs =
  39.107    let
  39.108 -    val ctxt = Proof_Context.init_global thy;
  39.109 +    val thy = Proof_Context.theory_of ctxt;
  39.110      val name = Sign.full_name thy b;
  39.111      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
  39.112        handle TERM (msg, _) => error msg;
  39.113      val lhs_const = Term.dest_Const (Term.head_of lhs);
  39.114      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
  39.115 -    val _ = check_overloading thy overloaded lhs_const;
  39.116 -  in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
  39.117 +    val _ = check_overloading ctxt overloaded lhs_const;
  39.118 +  in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
  39.119    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
  39.120     [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
  39.121 -    Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
  39.122 +    Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
  39.123  
  39.124  in
  39.125  
  39.126 -fun add_def unchecked overloaded raw_axm thy =
  39.127 -  let val axm = cert_axm thy raw_axm in
  39.128 +fun add_def ctxt unchecked overloaded raw_axm thy =
  39.129 +  let val axm = cert_axm ctxt raw_axm in
  39.130      thy
  39.131 -    |> map_defs (check_def thy unchecked overloaded axm)
  39.132 -    |> add_axiom axm
  39.133 +    |> map_defs (check_def ctxt unchecked overloaded axm)
  39.134 +    |> add_axiom ctxt axm
  39.135    end;
  39.136  
  39.137  end;
  39.138 @@ -270,18 +272,20 @@
  39.139  
  39.140  fun gen_add_finals prep_term overloaded args thy =
  39.141    let
  39.142 +    val ctxt = Syntax.init_pretty_global thy;
  39.143      fun const_of (Const const) = const
  39.144        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
  39.145        | const_of _ = error "Attempt to finalize non-constant term";
  39.146 -    fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
  39.147 -    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
  39.148 -      Sign.cert_term thy o prep_term thy;
  39.149 +    fun specify (c, T) = dependencies ctxt false NONE (c ^ " axiom") (c, T) [];
  39.150 +    val finalize =
  39.151 +      specify o tap (check_overloading ctxt overloaded) o const_of o
  39.152 +        Sign.cert_term thy o prep_term ctxt;
  39.153    in thy |> map_defs (fold finalize args) end;
  39.154  
  39.155  in
  39.156  
  39.157  val add_finals_i = gen_add_finals (K I);
  39.158 -val add_finals = gen_add_finals Syntax.read_term_global;
  39.159 +val add_finals = gen_add_finals Syntax.read_term;
  39.160  
  39.161  end;
  39.162  
    40.1 --- a/src/Pure/thm.ML	Sun Apr 17 13:47:22 2011 +0200
    40.2 +++ b/src/Pure/thm.ML	Sun Apr 17 19:54:04 2011 +0200
    40.3 @@ -1740,7 +1740,8 @@
    40.4  fun add_oracle (b, oracle) thy =
    40.5    let
    40.6      val naming = Sign.naming_of thy;
    40.7 -    val (name, tab') = Name_Space.define true naming (b, ()) (Oracles.get thy);
    40.8 +    val (name, tab') =
    40.9 +      Name_Space.define (Proof_Context.init_global thy) true naming (b, ()) (Oracles.get thy);
   40.10      val thy' = Oracles.put tab' thy;
   40.11    in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;
   40.12  
    41.1 --- a/src/Pure/type.ML	Sun Apr 17 13:47:22 2011 +0200
    41.2 +++ b/src/Pure/type.ML	Sun Apr 17 19:54:04 2011 +0200
    41.3 @@ -86,12 +86,13 @@
    41.4    val eq_type: tyenv -> typ * typ -> bool
    41.5  
    41.6    (*extend and merge type signatures*)
    41.7 -  val add_class: Pretty.pp -> Name_Space.naming -> binding * class list -> tsig -> tsig
    41.8 +  val add_class: Proof.context -> Pretty.pp -> Name_Space.naming ->
    41.9 +    binding * class list -> tsig -> tsig
   41.10    val hide_class: bool -> string -> tsig -> tsig
   41.11    val set_defsort: sort -> tsig -> tsig
   41.12 -  val add_type: Name_Space.naming -> binding * int -> tsig -> tsig
   41.13 -  val add_abbrev: Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   41.14 -  val add_nonterminal: Name_Space.naming -> binding -> tsig -> tsig
   41.15 +  val add_type: Proof.context -> Name_Space.naming -> binding * int -> tsig -> tsig
   41.16 +  val add_abbrev: Proof.context -> Name_Space.naming -> binding * string list * typ -> tsig -> tsig
   41.17 +  val add_nonterminal: Proof.context -> Name_Space.naming -> binding -> tsig -> tsig
   41.18    val hide_type: bool -> string -> tsig -> tsig
   41.19    val add_arity: Pretty.pp -> arity -> tsig -> tsig
   41.20    val add_classrel: Pretty.pp -> class * class -> tsig -> tsig
   41.21 @@ -576,13 +577,13 @@
   41.22  
   41.23  (* classes *)
   41.24  
   41.25 -fun add_class pp naming (c, cs) tsig =
   41.26 +fun add_class ctxt pp naming (c, cs) tsig =
   41.27    tsig |> map_tsig (fn ((space, classes), default, types) =>
   41.28      let
   41.29        val cs' = map (cert_class tsig) cs
   41.30          handle TYPE (msg, _, _) => error msg;
   41.31        val _ = Binding.check c;
   41.32 -      val (c', space') = space |> Name_Space.declare true naming c;
   41.33 +      val (c', space') = space |> Name_Space.declare ctxt true naming c;
   41.34        val classes' = classes |> Sorts.add_class pp (c', cs');
   41.35      in ((space', classes'), default, types) end);
   41.36  
   41.37 @@ -626,8 +627,8 @@
   41.38  
   41.39  local
   41.40  
   41.41 -fun new_decl naming (c, decl) types =
   41.42 -  (Binding.check c; #2 (Name_Space.define true naming (c, decl) types));
   41.43 +fun new_decl ctxt naming (c, decl) types =
   41.44 +  (Binding.check c; #2 (Name_Space.define ctxt true naming (c, decl) types));
   41.45  
   41.46  fun map_types f = map_tsig (fn (classes, default, types) =>
   41.47    let
   41.48 @@ -643,11 +644,11 @@
   41.49  
   41.50  in
   41.51  
   41.52 -fun add_type naming (c, n) =
   41.53 +fun add_type ctxt naming (c, n) =
   41.54    if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
   41.55 -  else map_types (new_decl naming (c, LogicalType n));
   41.56 +  else map_types (new_decl ctxt naming (c, LogicalType n));
   41.57  
   41.58 -fun add_abbrev naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   41.59 +fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   41.60    let
   41.61      fun err msg =
   41.62        cat_error msg ("The error(s) above occurred in type abbreviation " ^
   41.63 @@ -662,9 +663,9 @@
   41.64        (case subtract (op =) vs (map #1 (Term.add_tfreesT rhs' [])) of
   41.65          [] => []
   41.66        | extras => err ("Extra variables on rhs: " ^ commas_quote extras));
   41.67 -  in types |> new_decl naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
   41.68 +  in types |> new_decl ctxt naming (a, Abbreviation (vs, rhs', syntactic (#2 types) rhs')) end);
   41.69  
   41.70 -fun add_nonterminal naming = map_types o new_decl naming o rpair Nonterminal;
   41.71 +fun add_nonterminal ctxt naming = map_types o new_decl ctxt naming o rpair Nonterminal;
   41.72  
   41.73  end;
   41.74