report Name_Space.declare/define, relatively to context;
added "global" variants of context-dependent declarations;
--- 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)) =
--- 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
--- 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, _)) =
--- 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
--- 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
--- 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 =
--- 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;
--- 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;
--- 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')
--- 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)),
--- 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;
--- 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
--- 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 =
--- 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);
--- 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 *)
--- 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
--- 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;
--- 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);
--- 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;
--- 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 =
--- 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
--- 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),
--- 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 *)
--- 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))
--- 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))
--- 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')
--- 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, [])])));
--- 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;
--- 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),
--- 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)),
--- 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;
--- 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)
--- 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;
--- 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
--- 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 **)
--- 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;
--- 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)];
--- 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;
--- 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;
--- 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;
--- 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;