more explicit Defs.context: use proper name spaces as far as possible;

--- 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}
 

--- 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;
 
 

--- 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;
 

--- 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;

--- 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)

--- 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 =

--- 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";

--- 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;
 

--- 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

--- 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;
 
 
 

--- 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;