# HG changeset patch # User wenzelm # Date 1443130409 -7200 # Node ID ddb2da7cb2e44042263714e97cfbe9944bda54a1 # Parent e6f03fae14d59862a4687ea67d9383a0f4a08d00 more explicit Defs.context: use proper name spaces as far as possible; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Doc/Implementation/Logic.thy --- a/src/Doc/Implementation/Logic.thy Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Doc/Implementation/Logic.thy Thu Sep 24 23:33:29 2015 +0200 @@ -662,11 +662,11 @@ binding * term -> theory -> (string * thm) * theory"} \\ @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory"} \\ - @{index_ML Thm.add_def: "Proof.context -> bool -> bool -> + @{index_ML Thm.add_def: "Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory"} \\ \end{mldecls} \begin{mldecls} - @{index_ML Theory.add_deps: "Proof.context -> string -> + @{index_ML Theory.add_deps: "Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory"} \\ \end{mldecls} diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/HOL/Tools/typedef.ML Thu Sep 24 23:33:29 2015 +0200 @@ -138,6 +138,7 @@ (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>> Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn)); val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy); + val defs_context = Proof_Context.defs_context consts_lthy; val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A []; val A_types = @@ -149,9 +150,9 @@ val ((axiom_name, axiom), axiom_lthy) = consts_lthy |> Local_Theory.background_theory_result (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##> - Theory.add_deps consts_lthy "" newT_dep typedef_deps ##> - Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##> - Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]); + Theory.add_deps defs_context "" newT_dep typedef_deps ##> + Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##> + Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]); val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy); val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep)); @@ -166,7 +167,8 @@ Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."), Pretty.block [Pretty.str " Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT], Pretty.block (Pretty.str " Deps:" :: Pretty.brk 2 :: - Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))])) + Pretty.commas + (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))])) in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/Isar/generic_target.ML Thu Sep 24 23:33:29 2015 +0200 @@ -162,7 +162,7 @@ val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result - (Thm.add_def lthy2 false false + (Thm.add_def (Proof_Context.defs_context lthy2) false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))); in ((lhs, def), lthy3) end; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Sep 24 23:33:29 2015 +0200 @@ -44,6 +44,7 @@ val class_space: Proof.context -> Name_Space.T val type_space: Proof.context -> Name_Space.T val const_space: Proof.context -> Name_Space.T + val defs_context: Proof.context -> Defs.context val intern_class: Proof.context -> xstring -> string val intern_type: Proof.context -> xstring -> string val intern_const: Proof.context -> xstring -> string @@ -322,6 +323,8 @@ val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; +fun defs_context ctxt = (ctxt, SOME (const_space ctxt, type_space ctxt)); + val intern_class = Name_Space.intern o class_space; val intern_type = Name_Space.intern o type_space; val intern_const = Name_Space.intern o const_space; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/Isar/proof_display.ML Thu Sep 24 23:33:29 2015 +0200 @@ -82,25 +82,25 @@ fun pretty_definitions verbose ctxt = let val thy = Proof_Context.theory_of ctxt; + val context = Proof_Context.defs_context ctxt; val const_space = Proof_Context.const_space ctxt; val type_space = Proof_Context.type_space ctxt; val item_space = fn Defs.Const => const_space | Defs.Type => type_space; fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c; - fun markup_extern_item (kind, name) = - let val (markup, xname) = Name_Space.markup_extern ctxt (item_space kind) name - in (markup, (kind, xname)) end; + fun extern_item (kind, name) = + let val xname = Name_Space.extern ctxt (item_space kind) name + in (xname, (kind, name)) end; - fun pretty_entry ((markup, (kind, xname)), args) = - let - val prt_prefix = - if kind = Defs.Type then [Pretty.keyword1 "type", Pretty.brk 1] else []; - val prt_item = Pretty.mark_str (markup, xname); - val prt_args = Defs.pretty_args ctxt args; - in Pretty.block (prt_prefix @ [prt_item] @ prt_args) end; + fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) = + (case Defs.item_kind_ord (kind1, kind2) of + EQUAL => string_ord (xname1, xname2) + | ord => ord); - fun sort_items f = sort (Defs.item_ord o apply2 (snd o f)); + fun sort_items f = sort (extern_item_ord o apply2 f); + + fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args); fun pretty_reduct (lhs, rhs) = Pretty.block ([pretty_entry lhs, Pretty.str " ->", Pretty.brk 2] @ @@ -115,12 +115,12 @@ val (reds1, reds2) = filter_out (prune_item o #1 o #1) reducts |> map (fn (lhs, rhs) => - (apfst markup_extern_item lhs, map (apfst markup_extern_item) (filter_out (prune_item o fst) rhs))) + (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs))) |> sort_items (#1 o #1) |> filter_out (null o #2) |> List.partition (Defs.plain_args o #2 o #1); - val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1); + val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1); in Pretty.big_list "definitions:" (map (Pretty.text_fold o single) diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/Isar/typedecl.ML Thu Sep 24 23:33:29 2015 +0200 @@ -62,7 +62,8 @@ val c = Local_Theory.full_name lthy b; val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n); in - Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy + Local_Theory.background_theory + (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy end; fun basic_typedecl {final} (b, n, mx) lthy = diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/ROOT.ML Thu Sep 24 23:33:29 2015 +0200 @@ -170,8 +170,8 @@ use "envir.ML"; use "consts.ML"; use "primitive_defs.ML"; +use "sign.ML"; use "defs.ML"; -use "sign.ML"; use "term_sharing.ML"; use "pattern.ML"; use "unify.ML"; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/defs.ML --- a/src/Pure/defs.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/defs.ML Thu Sep 24 23:33:29 2015 +0200 @@ -9,11 +9,14 @@ sig datatype item_kind = Const | Type type item = item_kind * string - val item_ord: item * item -> order type entry = item * typ list + val item_kind_ord: item_kind * item_kind -> order + val plain_args: typ list -> bool + type context = Proof.context * (Name_Space.T * Name_Space.T) option + val space: context -> item_kind -> Name_Space.T + val pretty_item: context -> item -> Pretty.T val pretty_args: Proof.context -> typ list -> Pretty.T list - val pretty_entry: Proof.context -> entry -> Pretty.T - val plain_args: typ list -> bool + val pretty_entry: context -> entry -> Pretty.T type T type spec = {def: string option, @@ -27,8 +30,8 @@ {restricts: (entry * string) list, reducts: (entry * entry list) list} val empty: T - val merge: Proof.context -> T * T -> T - val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T + val merge: context -> T * T -> T + val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T val get_deps: T -> item -> (typ list * entry list) list end; @@ -39,29 +42,41 @@ datatype item_kind = Const | Type; type item = item_kind * string; +type entry = item * typ list; fun item_kind_ord (Const, Type) = LESS | item_kind_ord (Type, Const) = GREATER | item_kind_ord _ = EQUAL; -val item_ord = prod_ord item_kind_ord string_ord; -val fast_item_ord = prod_ord item_kind_ord fast_string_ord; - -fun print_item (k, s) = if k = Const then s else "type " ^ s; - -structure Itemtab = Table(type key = item val ord = fast_item_ord); +structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord); -(* type arguments *) +(* pretty printing *) + +type context = Proof.context * (Name_Space.T * Name_Space.T) option; -type entry = item * typ list; +fun space (ctxt, spaces) kind = + (case (kind, spaces) of + (Const, SOME (const_space, _)) => const_space + | (Type, SOME (_, type_space)) => type_space + | (Const, NONE) => Sign.const_space (Proof_Context.theory_of ctxt) + | (Type, NONE) => Sign.type_space (Proof_Context.theory_of ctxt)); + +fun pretty_item (context as (ctxt, _)) (kind, name) = + let val prt_name = Name_Space.pretty ctxt (space context kind) name in + if kind = Const then prt_name + else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name] + end; fun pretty_args ctxt args = if null args then [] else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)]; -fun pretty_entry ctxt (c, args) = - Pretty.block (Pretty.str (print_item c) :: pretty_args ctxt args); +fun pretty_entry context (c, args) = + Pretty.block (pretty_item context c :: pretty_args (#1 context) args); + + +(* type arguments *) fun plain_args args = forall Term.is_TVar args andalso not (has_duplicates (op =) args); @@ -129,21 +144,22 @@ (* specifications *) -fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = +fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) = Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) => i = j orelse disjoint_args (Ts, Us) orelse - error ("Clash of specifications for " ^ print_item c ^ ":\n" ^ + error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^ " " ^ quote a ^ Position.here pos_a ^ "\n" ^ " " ^ quote b ^ Position.here pos_b)); -fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = +fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) = let val specs' = - Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1; + Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2)) + specs2 specs1; in make_def (specs', restricts, reducts) end; -fun update_specs c spec = map_def c (fn (specs, restricts, reducts) => - (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts))); +fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) => + (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts))); (* normalized dependencies: reduction with well-formedness check *) @@ -151,23 +167,24 @@ local val prt = Pretty.string_of oo pretty_entry; -fun err ctxt (c, args) (d, Us) s1 s2 = - error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2); -fun acyclic ctxt (c, args) (d, Us) = +fun err context (c, args) (d, Us) s1 s2 = + error (s1 ^ " dependency of " ^ prt context (c, args) ^ " -> " ^ prt context (d, Us) ^ s2); + +fun acyclic context (c, args) (d, Us) = c <> d orelse is_none (match_args (args, Us)) orelse - err ctxt (c, args) (d, Us) "Circular" ""; + err context (c, args) (d, Us) "Circular" ""; -fun wellformed ctxt defs (c, args) (d, Us) = +fun wellformed context defs (c, args) (d, Us) = plain_args Us orelse (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of SOME (Ts, description) => - err ctxt (c, args) (d, Us) "Malformed" - ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")") + err context (c, args) (d, Us) "Malformed" + ("\n(restriction " ^ prt context (d, Ts) ^ " from " ^ quote description ^ ")") | NONE => true); -fun reduction ctxt defs const deps = +fun reduction context defs const deps = let fun reduct Us (Ts, rhs) = (case match_args (Ts, Us) of @@ -180,17 +197,17 @@ if forall (is_none o #1) reds then NONE else SOME (fold_rev (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []); - val _ = forall (acyclic ctxt const) (the_default deps deps'); + val _ = forall (acyclic context const) (the_default deps deps'); in deps' end; in -fun normalize ctxt = +fun normalize context = let fun norm_update (c, {reducts, ...}: def) (changed, defs) = let val reducts' = reducts |> map (fn (args, deps) => - (args, perhaps (reduction ctxt defs (c, args)) deps)); + (args, perhaps (reduction context defs (c, args)) deps)); in if reducts = reducts' then (changed, defs) else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts'))) @@ -200,38 +217,38 @@ (true, defs') => norm_all defs' | (false, _) => defs); fun check defs (c, {reducts, ...}: def) = - reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps); + reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps); in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end; -fun dependencies ctxt (c, args) restr deps = +fun dependencies context (c, args) restr deps = map_def c (fn (specs, restricts, reducts) => let val restricts' = Library.merge (op =) (restricts, restr); val reducts' = insert (op =) (args, deps) reducts; in (specs, restricts', reducts') end) - #> normalize ctxt; + #> normalize context; end; (* merge *) -fun merge ctxt (Defs defs1, Defs defs2) = +fun merge context (Defs defs1, Defs defs2) = let fun add_deps (c, args) restr deps defs = if AList.defined (op =) (reducts_of defs c) args then defs - else dependencies ctxt (c, args) restr deps defs; + else dependencies context (c, args) restr deps defs; fun add_def (c, {restricts, reducts, ...}: def) = fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts; in - Defs (Itemtab.join join_specs (defs1, defs2) - |> normalize ctxt |> Itemtab.fold add_def defs2) + Defs (Itemtab.join (join_specs context) (defs1, defs2) + |> normalize context |> Itemtab.fold add_def defs2) end; (* define *) -fun define ctxt unchecked def description (c, args) deps (Defs defs) = +fun define context unchecked def description (c, args) deps (Defs defs) = let val pos = Position.thread_data (); val restr = @@ -240,8 +257,8 @@ then [] else [(args, description)]; val spec = (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps}); - val defs' = defs |> update_specs c spec; - in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end; + val defs' = defs |> update_specs context c spec; + in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end; fun get_deps (Defs defs) c = reducts_of defs c; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/global_theory.ML --- a/src/Pure/global_theory.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/global_theory.ML Thu Sep 24 23:33:29 2015 +0200 @@ -207,7 +207,7 @@ let 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 ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy; val thm = def |> Thm.forall_intr_frees |> Thm.forall_elim_vars 0 diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/more_thm.ML --- a/src/Pure/more_thm.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/more_thm.ML Thu Sep 24 23:33:29 2015 +0200 @@ -72,7 +72,7 @@ val rename_boundvars: term -> term -> thm -> thm 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: Defs.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 option * thm option type binding = binding * attribute list @@ -475,13 +475,13 @@ fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy; -fun add_def ctxt unchecked overloaded (b, prop) thy = +fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy = let val _ = Sign.no_vars ctxt prop; val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop); val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop); - val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy; + val thy' = Theory.add_def context unchecked overloaded (b, concl') thy; val axm_name = Sign.full_name thy' b; val axm' = Thm.axiom thy' axm_name; val thm = @@ -491,7 +491,7 @@ 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; + add_def (Syntax.init_pretty_global thy, NONE) unchecked overloaded arg thy; diff -r e6f03fae14d5 -r ddb2da7cb2e4 src/Pure/theory.ML --- a/src/Pure/theory.ML Thu Sep 24 13:33:42 2015 +0200 +++ b/src/Pure/theory.ML Thu Sep 24 23:33:29 2015 +0200 @@ -25,9 +25,9 @@ val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry - val add_deps: Proof.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory + val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory - val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory + val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end @@ -75,12 +75,11 @@ fun merge pp (thy1, thy2) = let - val ctxt = Syntax.init_pretty pp; val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1; val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2; val axioms' = empty_axioms; - val defs' = Defs.merge ctxt (defs1, defs2); + val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end; @@ -216,7 +215,7 @@ fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); -fun dependencies ctxt unchecked def description lhs rhs = +fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let val thy = Proof_Context.theory_of ctxt; val consts = Sign.consts_of thy; @@ -235,7 +234,7 @@ else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); - in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end; + in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) @@ -243,14 +242,14 @@ | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; -fun add_deps ctxt a raw_lhs raw_rhs thy = +fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; - in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end; + in thy |> map_defs (dependencies context 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; + add_deps (Syntax.init_pretty_global thy, NONE) a x y thy; fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; @@ -286,7 +285,7 @@ local -fun check_def ctxt thy unchecked overloaded (b, tm) defs = +fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm @@ -300,17 +299,17 @@ val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; - in defs |> dependencies ctxt unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end + in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in -fun add_def ctxt unchecked overloaded raw_axm thy = +fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy - |> map_defs (check_def ctxt thy unchecked overloaded axm) + |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end;