more explicit Defs.context: use proper name spaces as far as possible;
authorwenzelm
Thu Sep 24 23:33:29 2015 +0200 (2015-09-24)
changeset 61261ddb2da7cb2e4
parent 61260 e6f03fae14d5
child 61262 7bd1eb4b056e
more explicit Defs.context: use proper name spaces as far as possible;
src/Doc/Implementation/Logic.thy
src/HOL/Tools/typedef.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/proof_display.ML
src/Pure/Isar/typedecl.ML
src/Pure/ROOT.ML
src/Pure/defs.ML
src/Pure/global_theory.ML
src/Pure/more_thm.ML
src/Pure/theory.ML
     1.1 --- a/src/Doc/Implementation/Logic.thy	Thu Sep 24 13:33:42 2015 +0200
     1.2 +++ b/src/Doc/Implementation/Logic.thy	Thu Sep 24 23:33:29 2015 +0200
     1.3 @@ -662,11 +662,11 @@
     1.4    binding * term -> theory -> (string * thm) * theory"} \\
     1.5    @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
     1.6    (string * ('a -> thm)) * theory"} \\
     1.7 -  @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
     1.8 +  @{index_ML Thm.add_def: "Defs.context -> bool -> bool ->
     1.9    binding * term -> theory -> (string * thm) * theory"} \\
    1.10    \end{mldecls}
    1.11    \begin{mldecls}
    1.12 -  @{index_ML Theory.add_deps: "Proof.context -> string ->
    1.13 +  @{index_ML Theory.add_deps: "Defs.context -> string ->
    1.14    Defs.entry -> Defs.entry list -> theory -> theory"} \\
    1.15    \end{mldecls}
    1.16  
     2.1 --- a/src/HOL/Tools/typedef.ML	Thu Sep 24 13:33:42 2015 +0200
     2.2 +++ b/src/HOL/Tools/typedef.ML	Thu Sep 24 23:33:29 2015 +0200
     2.3 @@ -138,6 +138,7 @@
     2.4          (Sign.declare_const lthy ((Rep_name, newT --> oldT), NoSyn) ##>>
     2.5            Sign.declare_const lthy ((Abs_name, oldT --> newT), NoSyn));
     2.6      val const_dep = Theory.const_dep (Proof_Context.theory_of consts_lthy);
     2.7 +    val defs_context = Proof_Context.defs_context consts_lthy;
     2.8  
     2.9      val A_consts = fold_aterms (fn Const c => insert (op =) (const_dep c) | _ => I) A [];
    2.10      val A_types =
    2.11 @@ -149,9 +150,9 @@
    2.12      val ((axiom_name, axiom), axiom_lthy) = consts_lthy
    2.13        |> Local_Theory.background_theory_result
    2.14          (Thm.add_axiom consts_lthy (type_definition_name, mk_typedef newT oldT RepC AbsC A) ##>
    2.15 -          Theory.add_deps consts_lthy "" newT_dep typedef_deps ##>
    2.16 -          Theory.add_deps consts_lthy "" (const_dep (dest_Const RepC)) [newT_dep] ##>
    2.17 -          Theory.add_deps consts_lthy "" (const_dep (dest_Const AbsC)) [newT_dep]);
    2.18 +          Theory.add_deps defs_context "" newT_dep typedef_deps ##>
    2.19 +          Theory.add_deps defs_context "" (const_dep (dest_Const RepC)) [newT_dep] ##>
    2.20 +          Theory.add_deps defs_context "" (const_dep (dest_Const AbsC)) [newT_dep]);
    2.21  
    2.22      val axiom_defs = Theory.defs_of (Proof_Context.theory_of axiom_lthy);
    2.23      val newT_deps = maps #2 (Defs.get_deps axiom_defs (#1 newT_dep));
    2.24 @@ -166,7 +167,8 @@
    2.25               Pretty.text "or enable configuration option \"typedef_overloaded\" in the context."),
    2.26             Pretty.block [Pretty.str "  Type:", Pretty.brk 2, Syntax.pretty_typ axiom_lthy newT],
    2.27             Pretty.block (Pretty.str "  Deps:" :: Pretty.brk 2 ::
    2.28 -             Pretty.commas (map (Defs.pretty_entry axiom_lthy) newT_deps))]))
    2.29 +             Pretty.commas
    2.30 +              (map (Defs.pretty_entry (Proof_Context.defs_context axiom_lthy)) newT_deps))]))
    2.31    in ((RepC, AbsC, axiom_name, axiom), axiom_lthy) end;
    2.32  
    2.33  
     3.1 --- a/src/Pure/Isar/generic_target.ML	Thu Sep 24 13:33:42 2015 +0200
     3.2 +++ b/src/Pure/Isar/generic_target.ML	Thu Sep 24 23:33:29 2015 +0200
     3.3 @@ -162,7 +162,7 @@
     3.4  
     3.5      val ((_, def), lthy3) = lthy2
     3.6        |> Local_Theory.background_theory_result
     3.7 -        (Thm.add_def lthy2 false false
     3.8 +        (Thm.add_def (Proof_Context.defs_context lthy2) false false
     3.9            (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
    3.10    in ((lhs, def), lthy3) end;
    3.11  
     4.1 --- a/src/Pure/Isar/proof_context.ML	Thu Sep 24 13:33:42 2015 +0200
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Sep 24 23:33:29 2015 +0200
     4.3 @@ -44,6 +44,7 @@
     4.4    val class_space: Proof.context -> Name_Space.T
     4.5    val type_space: Proof.context -> Name_Space.T
     4.6    val const_space: Proof.context -> Name_Space.T
     4.7 +  val defs_context: Proof.context -> Defs.context
     4.8    val intern_class: Proof.context -> xstring -> string
     4.9    val intern_type: Proof.context -> xstring -> string
    4.10    val intern_const: Proof.context -> xstring -> string
    4.11 @@ -322,6 +323,8 @@
    4.12  val type_space = Type.type_space o tsig_of;
    4.13  val const_space = Consts.space_of o consts_of;
    4.14  
    4.15 +fun defs_context ctxt = (ctxt, SOME (const_space ctxt, type_space ctxt));
    4.16 +
    4.17  val intern_class = Name_Space.intern o class_space;
    4.18  val intern_type = Name_Space.intern o type_space;
    4.19  val intern_const = Name_Space.intern o const_space;
     5.1 --- a/src/Pure/Isar/proof_display.ML	Thu Sep 24 13:33:42 2015 +0200
     5.2 +++ b/src/Pure/Isar/proof_display.ML	Thu Sep 24 23:33:29 2015 +0200
     5.3 @@ -82,25 +82,25 @@
     5.4  fun pretty_definitions verbose ctxt =
     5.5    let
     5.6      val thy = Proof_Context.theory_of ctxt;
     5.7 +    val context = Proof_Context.defs_context ctxt;
     5.8  
     5.9      val const_space = Proof_Context.const_space ctxt;
    5.10      val type_space = Proof_Context.type_space ctxt;
    5.11      val item_space = fn Defs.Const => const_space | Defs.Type => type_space;
    5.12      fun prune_item (k, c) = not verbose andalso Name_Space.is_concealed (item_space k) c;
    5.13  
    5.14 -    fun markup_extern_item (kind, name) =
    5.15 -      let val (markup, xname) = Name_Space.markup_extern ctxt (item_space kind) name
    5.16 -      in (markup, (kind, xname)) end;
    5.17 +    fun extern_item (kind, name) =
    5.18 +      let val xname = Name_Space.extern ctxt (item_space kind) name
    5.19 +      in (xname, (kind, name)) end;
    5.20  
    5.21 -    fun pretty_entry ((markup, (kind, xname)), args) =
    5.22 -      let
    5.23 -        val prt_prefix =
    5.24 -          if kind = Defs.Type then [Pretty.keyword1 "type", Pretty.brk 1] else [];
    5.25 -        val prt_item = Pretty.mark_str (markup, xname);
    5.26 -        val prt_args = Defs.pretty_args ctxt args;
    5.27 -      in Pretty.block (prt_prefix @ [prt_item] @ prt_args) end;
    5.28 +    fun extern_item_ord ((xname1, (kind1, _)), (xname2, (kind2, _))) =
    5.29 +      (case Defs.item_kind_ord (kind1, kind2) of
    5.30 +        EQUAL => string_ord (xname1, xname2)
    5.31 +      | ord => ord);
    5.32  
    5.33 -    fun sort_items f = sort (Defs.item_ord o apply2 (snd o f));
    5.34 +    fun sort_items f = sort (extern_item_ord o apply2 f);
    5.35 +
    5.36 +    fun pretty_entry ((_: string, item), args) = Defs.pretty_entry context (item, args);
    5.37  
    5.38      fun pretty_reduct (lhs, rhs) = Pretty.block
    5.39        ([pretty_entry lhs, Pretty.str "  ->", Pretty.brk 2] @
    5.40 @@ -115,12 +115,12 @@
    5.41      val (reds1, reds2) =
    5.42        filter_out (prune_item o #1 o #1) reducts
    5.43        |> map (fn (lhs, rhs) =>
    5.44 -        (apfst markup_extern_item lhs, map (apfst markup_extern_item) (filter_out (prune_item o fst) rhs)))
    5.45 +        (apfst extern_item lhs, map (apfst extern_item) (filter_out (prune_item o fst) rhs)))
    5.46        |> sort_items (#1 o #1)
    5.47        |> filter_out (null o #2)
    5.48        |> List.partition (Defs.plain_args o #2 o #1);
    5.49  
    5.50 -    val rests = restricts |> map (apfst (apfst markup_extern_item)) |> sort_items (#1 o #1);
    5.51 +    val rests = restricts |> map (apfst (apfst extern_item)) |> sort_items (#1 o #1);
    5.52    in
    5.53      Pretty.big_list "definitions:"
    5.54        (map (Pretty.text_fold o single)
     6.1 --- a/src/Pure/Isar/typedecl.ML	Thu Sep 24 13:33:42 2015 +0200
     6.2 +++ b/src/Pure/Isar/typedecl.ML	Thu Sep 24 23:33:29 2015 +0200
     6.3 @@ -62,7 +62,8 @@
     6.4      val c = Local_Theory.full_name lthy b;
     6.5      val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
     6.6    in
     6.7 -    Local_Theory.background_theory (Theory.add_deps lthy "" (Theory.type_dep (c, args)) []) lthy
     6.8 +    Local_Theory.background_theory
     6.9 +      (Theory.add_deps (Proof_Context.defs_context lthy) "" (Theory.type_dep (c, args)) []) lthy
    6.10    end;
    6.11  
    6.12  fun basic_typedecl {final} (b, n, mx) lthy =
     7.1 --- a/src/Pure/ROOT.ML	Thu Sep 24 13:33:42 2015 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Thu Sep 24 23:33:29 2015 +0200
     7.3 @@ -170,8 +170,8 @@
     7.4  use "envir.ML";
     7.5  use "consts.ML";
     7.6  use "primitive_defs.ML";
     7.7 +use "sign.ML";
     7.8  use "defs.ML";
     7.9 -use "sign.ML";
    7.10  use "term_sharing.ML";
    7.11  use "pattern.ML";
    7.12  use "unify.ML";
     8.1 --- a/src/Pure/defs.ML	Thu Sep 24 13:33:42 2015 +0200
     8.2 +++ b/src/Pure/defs.ML	Thu Sep 24 23:33:29 2015 +0200
     8.3 @@ -9,11 +9,14 @@
     8.4  sig
     8.5    datatype item_kind = Const | Type
     8.6    type item = item_kind * string
     8.7 -  val item_ord: item * item -> order
     8.8    type entry = item * typ list
     8.9 +  val item_kind_ord: item_kind * item_kind -> order
    8.10 +  val plain_args: typ list -> bool
    8.11 +  type context = Proof.context * (Name_Space.T * Name_Space.T) option
    8.12 +  val space: context -> item_kind -> Name_Space.T
    8.13 +  val pretty_item: context -> item -> Pretty.T
    8.14    val pretty_args: Proof.context -> typ list -> Pretty.T list
    8.15 -  val pretty_entry: Proof.context -> entry -> Pretty.T
    8.16 -  val plain_args: typ list -> bool
    8.17 +  val pretty_entry: context -> entry -> Pretty.T
    8.18    type T
    8.19    type spec =
    8.20     {def: string option,
    8.21 @@ -27,8 +30,8 @@
    8.22     {restricts: (entry * string) list,
    8.23      reducts: (entry * entry list) list}
    8.24    val empty: T
    8.25 -  val merge: Proof.context -> T * T -> T
    8.26 -  val define: Proof.context -> bool -> string option -> string -> entry -> entry list -> T -> T
    8.27 +  val merge: context -> T * T -> T
    8.28 +  val define: context -> bool -> string option -> string -> entry -> entry list -> T -> T
    8.29    val get_deps: T -> item -> (typ list * entry list) list
    8.30  end;
    8.31  
    8.32 @@ -39,29 +42,41 @@
    8.33  
    8.34  datatype item_kind = Const | Type;
    8.35  type item = item_kind * string;
    8.36 +type entry = item * typ list;
    8.37  
    8.38  fun item_kind_ord (Const, Type) = LESS
    8.39    | item_kind_ord (Type, Const) = GREATER
    8.40    | item_kind_ord _ = EQUAL;
    8.41  
    8.42 -val item_ord = prod_ord item_kind_ord string_ord;
    8.43 -val fast_item_ord = prod_ord item_kind_ord fast_string_ord;
    8.44 -
    8.45 -fun print_item (k, s) = if k = Const then s else "type " ^ s;
    8.46 -
    8.47 -structure Itemtab = Table(type key = item val ord = fast_item_ord);
    8.48 +structure Itemtab = Table(type key = item val ord = prod_ord item_kind_ord fast_string_ord);
    8.49  
    8.50  
    8.51 -(* type arguments *)
    8.52 +(* pretty printing *)
    8.53 +
    8.54 +type context = Proof.context * (Name_Space.T * Name_Space.T) option;
    8.55  
    8.56 -type entry = item * typ list;
    8.57 +fun space (ctxt, spaces) kind =
    8.58 +  (case (kind, spaces) of
    8.59 +    (Const, SOME (const_space, _)) => const_space
    8.60 +  | (Type, SOME (_, type_space)) => type_space
    8.61 +  | (Const, NONE) => Sign.const_space (Proof_Context.theory_of ctxt)
    8.62 +  | (Type, NONE) => Sign.type_space (Proof_Context.theory_of ctxt));
    8.63 +
    8.64 +fun pretty_item (context as (ctxt, _)) (kind, name) =
    8.65 +  let val prt_name = Name_Space.pretty ctxt (space context kind) name in
    8.66 +    if kind = Const then prt_name
    8.67 +    else Pretty.block [Pretty.keyword1 "type", Pretty.brk 1, prt_name]
    8.68 +  end;
    8.69  
    8.70  fun pretty_args ctxt args =
    8.71    if null args then []
    8.72    else [Pretty.list "(" ")" (map (Syntax.pretty_typ ctxt o Logic.unvarifyT_global) args)];
    8.73  
    8.74 -fun pretty_entry ctxt (c, args) =
    8.75 -  Pretty.block (Pretty.str (print_item c) :: pretty_args ctxt args);
    8.76 +fun pretty_entry context (c, args) =
    8.77 +  Pretty.block (pretty_item context c :: pretty_args (#1 context) args);
    8.78 +
    8.79 +
    8.80 +(* type arguments *)
    8.81  
    8.82  fun plain_args args =
    8.83    forall Term.is_TVar args andalso not (has_duplicates (op =) args);
    8.84 @@ -129,21 +144,22 @@
    8.85  
    8.86  (* specifications *)
    8.87  
    8.88 -fun disjoint_specs c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
    8.89 +fun disjoint_specs context c (i, {description = a, pos = pos_a, lhs = Ts, ...}: spec) =
    8.90    Inttab.forall (fn (j, {description = b, pos = pos_b, lhs = Us, ...}: spec) =>
    8.91      i = j orelse disjoint_args (Ts, Us) orelse
    8.92 -      error ("Clash of specifications for " ^ print_item c ^ ":\n" ^
    8.93 +      error ("Clash of specifications for " ^ Pretty.str_of (pretty_item context c) ^ ":\n" ^
    8.94          "  " ^ quote a ^ Position.here pos_a ^ "\n" ^
    8.95          "  " ^ quote b ^ Position.here pos_b));
    8.96  
    8.97 -fun join_specs c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
    8.98 +fun join_specs context c ({specs = specs1, restricts, reducts}, {specs = specs2, ...}: def) =
    8.99    let
   8.100      val specs' =
   8.101 -      Inttab.fold (fn spec2 => (disjoint_specs c spec2 specs1; Inttab.update spec2)) specs2 specs1;
   8.102 +      Inttab.fold (fn spec2 => (disjoint_specs context c spec2 specs1; Inttab.update spec2))
   8.103 +        specs2 specs1;
   8.104    in make_def (specs', restricts, reducts) end;
   8.105  
   8.106 -fun update_specs c spec = map_def c (fn (specs, restricts, reducts) =>
   8.107 -  (disjoint_specs c spec specs; (Inttab.update spec specs, restricts, reducts)));
   8.108 +fun update_specs context c spec = map_def c (fn (specs, restricts, reducts) =>
   8.109 +  (disjoint_specs context c spec specs; (Inttab.update spec specs, restricts, reducts)));
   8.110  
   8.111  
   8.112  (* normalized dependencies: reduction with well-formedness check *)
   8.113 @@ -151,23 +167,24 @@
   8.114  local
   8.115  
   8.116  val prt = Pretty.string_of oo pretty_entry;
   8.117 -fun err ctxt (c, args) (d, Us) s1 s2 =
   8.118 -  error (s1 ^ " dependency of " ^ prt ctxt (c, args) ^ " -> " ^ prt ctxt (d, Us) ^ s2);
   8.119  
   8.120 -fun acyclic ctxt (c, args) (d, Us) =
   8.121 +fun err context (c, args) (d, Us) s1 s2 =
   8.122 +  error (s1 ^ " dependency of " ^ prt context (c, args) ^ " -> " ^ prt context (d, Us) ^ s2);
   8.123 +
   8.124 +fun acyclic context (c, args) (d, Us) =
   8.125    c <> d orelse
   8.126    is_none (match_args (args, Us)) orelse
   8.127 -  err ctxt (c, args) (d, Us) "Circular" "";
   8.128 +  err context (c, args) (d, Us) "Circular" "";
   8.129  
   8.130 -fun wellformed ctxt defs (c, args) (d, Us) =
   8.131 +fun wellformed context defs (c, args) (d, Us) =
   8.132    plain_args Us orelse
   8.133    (case find_first (fn (Ts, _) => not (disjoint_args (Ts, Us))) (restricts_of defs d) of
   8.134      SOME (Ts, description) =>
   8.135 -      err ctxt (c, args) (d, Us) "Malformed"
   8.136 -        ("\n(restriction " ^ prt ctxt (d, Ts) ^ " from " ^ quote description ^ ")")
   8.137 +      err context (c, args) (d, Us) "Malformed"
   8.138 +        ("\n(restriction " ^ prt context (d, Ts) ^ " from " ^ quote description ^ ")")
   8.139    | NONE => true);
   8.140  
   8.141 -fun reduction ctxt defs const deps =
   8.142 +fun reduction context defs const deps =
   8.143    let
   8.144      fun reduct Us (Ts, rhs) =
   8.145        (case match_args (Ts, Us) of
   8.146 @@ -180,17 +197,17 @@
   8.147        if forall (is_none o #1) reds then NONE
   8.148        else SOME (fold_rev
   8.149          (fn (NONE, dp) => insert (op =) dp | (SOME dps, _) => fold (insert (op =)) dps) reds []);
   8.150 -    val _ = forall (acyclic ctxt const) (the_default deps deps');
   8.151 +    val _ = forall (acyclic context const) (the_default deps deps');
   8.152    in deps' end;
   8.153  
   8.154  in
   8.155  
   8.156 -fun normalize ctxt =
   8.157 +fun normalize context =
   8.158    let
   8.159      fun norm_update (c, {reducts, ...}: def) (changed, defs) =
   8.160        let
   8.161          val reducts' = reducts |> map (fn (args, deps) =>
   8.162 -          (args, perhaps (reduction ctxt defs (c, args)) deps));
   8.163 +          (args, perhaps (reduction context defs (c, args)) deps));
   8.164        in
   8.165          if reducts = reducts' then (changed, defs)
   8.166          else (true, defs |> map_def c (fn (specs, restricts, _) => (specs, restricts, reducts')))
   8.167 @@ -200,38 +217,38 @@
   8.168          (true, defs') => norm_all defs'
   8.169        | (false, _) => defs);
   8.170      fun check defs (c, {reducts, ...}: def) =
   8.171 -      reducts |> forall (fn (args, deps) => forall (wellformed ctxt defs (c, args)) deps);
   8.172 +      reducts |> forall (fn (args, deps) => forall (wellformed context defs (c, args)) deps);
   8.173    in norm_all #> (fn defs => tap (Itemtab.forall (check defs)) defs) end;
   8.174  
   8.175 -fun dependencies ctxt (c, args) restr deps =
   8.176 +fun dependencies context (c, args) restr deps =
   8.177    map_def c (fn (specs, restricts, reducts) =>
   8.178      let
   8.179        val restricts' = Library.merge (op =) (restricts, restr);
   8.180        val reducts' = insert (op =) (args, deps) reducts;
   8.181      in (specs, restricts', reducts') end)
   8.182 -  #> normalize ctxt;
   8.183 +  #> normalize context;
   8.184  
   8.185  end;
   8.186  
   8.187  
   8.188  (* merge *)
   8.189  
   8.190 -fun merge ctxt (Defs defs1, Defs defs2) =
   8.191 +fun merge context (Defs defs1, Defs defs2) =
   8.192    let
   8.193      fun add_deps (c, args) restr deps defs =
   8.194        if AList.defined (op =) (reducts_of defs c) args then defs
   8.195 -      else dependencies ctxt (c, args) restr deps defs;
   8.196 +      else dependencies context (c, args) restr deps defs;
   8.197      fun add_def (c, {restricts, reducts, ...}: def) =
   8.198        fold (fn (args, deps) => add_deps (c, args) restricts deps) reducts;
   8.199    in
   8.200 -    Defs (Itemtab.join join_specs (defs1, defs2)
   8.201 -      |> normalize ctxt |> Itemtab.fold add_def defs2)
   8.202 +    Defs (Itemtab.join (join_specs context) (defs1, defs2)
   8.203 +      |> normalize context |> Itemtab.fold add_def defs2)
   8.204    end;
   8.205  
   8.206  
   8.207  (* define *)
   8.208  
   8.209 -fun define ctxt unchecked def description (c, args) deps (Defs defs) =
   8.210 +fun define context unchecked def description (c, args) deps (Defs defs) =
   8.211    let
   8.212      val pos = Position.thread_data ();
   8.213      val restr =
   8.214 @@ -240,8 +257,8 @@
   8.215        then [] else [(args, description)];
   8.216      val spec =
   8.217        (serial (), {def = def, description = description, pos = pos, lhs = args, rhs = deps});
   8.218 -    val defs' = defs |> update_specs c spec;
   8.219 -  in Defs (defs' |> (if unchecked then I else dependencies ctxt (c, args) restr deps)) end;
   8.220 +    val defs' = defs |> update_specs context c spec;
   8.221 +  in Defs (defs' |> (if unchecked then I else dependencies context (c, args) restr deps)) end;
   8.222  
   8.223  fun get_deps (Defs defs) c = reducts_of defs c;
   8.224  
     9.1 --- a/src/Pure/global_theory.ML	Thu Sep 24 13:33:42 2015 +0200
     9.2 +++ b/src/Pure/global_theory.ML	Thu Sep 24 23:33:29 2015 +0200
     9.3 @@ -207,7 +207,7 @@
     9.4    let
     9.5      val ctxt = Syntax.init_pretty_global thy;
     9.6      val prop = prep ctxt (b, raw_prop);
     9.7 -    val ((_, def), thy') = Thm.add_def ctxt unchecked overloaded (b, prop) thy;
     9.8 +    val ((_, def), thy') = Thm.add_def (ctxt, NONE) unchecked overloaded (b, prop) thy;
     9.9      val thm = def
    9.10        |> Thm.forall_intr_frees
    9.11        |> Thm.forall_elim_vars 0
    10.1 --- a/src/Pure/more_thm.ML	Thu Sep 24 13:33:42 2015 +0200
    10.2 +++ b/src/Pure/more_thm.ML	Thu Sep 24 23:33:29 2015 +0200
    10.3 @@ -72,7 +72,7 @@
    10.4    val rename_boundvars: term -> term -> thm -> thm
    10.5    val add_axiom: Proof.context -> binding * term -> theory -> (string * thm) * theory
    10.6    val add_axiom_global: binding * term -> theory -> (string * thm) * theory
    10.7 -  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
    10.8 +  val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> (string * thm) * theory
    10.9    val add_def_global: bool -> bool -> binding * term -> theory -> (string * thm) * theory
   10.10    type attribute = Context.generic * thm -> Context.generic option * thm option
   10.11    type binding = binding * attribute list
   10.12 @@ -475,13 +475,13 @@
   10.13  
   10.14  fun add_axiom_global arg thy = add_axiom (Syntax.init_pretty_global thy) arg thy;
   10.15  
   10.16 -fun add_def ctxt unchecked overloaded (b, prop) thy =
   10.17 +fun add_def (context as (ctxt, _)) unchecked overloaded (b, prop) thy =
   10.18    let
   10.19      val _ = Sign.no_vars ctxt prop;
   10.20      val prems = map (Thm.cterm_of ctxt) (Logic.strip_imp_prems prop);
   10.21      val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
   10.22  
   10.23 -    val thy' = Theory.add_def ctxt unchecked overloaded (b, concl') thy;
   10.24 +    val thy' = Theory.add_def context unchecked overloaded (b, concl') thy;
   10.25      val axm_name = Sign.full_name thy' b;
   10.26      val axm' = Thm.axiom thy' axm_name;
   10.27      val thm =
   10.28 @@ -491,7 +491,7 @@
   10.29    in ((axm_name, thm), thy') end;
   10.30  
   10.31  fun add_def_global unchecked overloaded arg thy =
   10.32 -  add_def (Syntax.init_pretty_global thy) unchecked overloaded arg thy;
   10.33 +  add_def (Syntax.init_pretty_global thy, NONE) unchecked overloaded arg thy;
   10.34  
   10.35  
   10.36  
    11.1 --- a/src/Pure/theory.ML	Thu Sep 24 13:33:42 2015 +0200
    11.2 +++ b/src/Pure/theory.ML	Thu Sep 24 23:33:29 2015 +0200
    11.3 @@ -25,9 +25,9 @@
    11.4    val add_axiom: Proof.context -> binding * term -> theory -> theory
    11.5    val const_dep: theory -> string * typ -> Defs.entry
    11.6    val type_dep: string * typ list -> Defs.entry
    11.7 -  val add_deps: Proof.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
    11.8 +  val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
    11.9    val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
   11.10 -  val add_def: Proof.context -> bool -> bool -> binding * term -> theory -> theory
   11.11 +  val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   11.12    val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   11.13    val check_overloading: Proof.context -> bool -> string * typ -> unit
   11.14  end
   11.15 @@ -75,12 +75,11 @@
   11.16  
   11.17    fun merge pp (thy1, thy2) =
   11.18      let
   11.19 -      val ctxt = Syntax.init_pretty pp;
   11.20        val Thy {pos = _, id = _, axioms = _, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
   11.21        val Thy {pos = _, id = _, axioms = _, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
   11.22  
   11.23        val axioms' = empty_axioms;
   11.24 -      val defs' = Defs.merge ctxt (defs1, defs2);
   11.25 +      val defs' = Defs.merge (Syntax.init_pretty pp, NONE) (defs1, defs2);
   11.26        val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
   11.27        val ens' = Library.merge (eq_snd op =) (ens1, ens2);
   11.28      in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end;
   11.29 @@ -216,7 +215,7 @@
   11.30  fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T));
   11.31  fun type_dep (c, args) = ((Defs.Type, c), args);
   11.32  
   11.33 -fun dependencies ctxt unchecked def description lhs rhs =
   11.34 +fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs =
   11.35    let
   11.36      val thy = Proof_Context.theory_of ctxt;
   11.37      val consts = Sign.consts_of thy;
   11.38 @@ -235,7 +234,7 @@
   11.39        else error ("Specification depends on extra type variables: " ^
   11.40          commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^
   11.41          "\nThe error(s) above occurred in " ^ quote description);
   11.42 -  in Defs.define ctxt unchecked def description (prep lhs) (map prep rhs) end;
   11.43 +  in Defs.define context unchecked def description (prep lhs) (map prep rhs) end;
   11.44  
   11.45  fun cert_entry thy ((Defs.Const, c), args) =
   11.46        Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args)))
   11.47 @@ -243,14 +242,14 @@
   11.48    | cert_entry thy ((Defs.Type, c), args) =
   11.49        Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep;
   11.50  
   11.51 -fun add_deps ctxt a raw_lhs raw_rhs thy =
   11.52 +fun add_deps context a raw_lhs raw_rhs thy =
   11.53    let
   11.54      val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs);
   11.55      val description = if a = "" then lhs_name ^ " axiom" else a;
   11.56 -  in thy |> map_defs (dependencies ctxt false NONE description lhs rhs) end;
   11.57 +  in thy |> map_defs (dependencies context false NONE description lhs rhs) end;
   11.58  
   11.59  fun add_deps_global a x y thy =
   11.60 -  add_deps (Syntax.init_pretty_global thy) a x y thy;
   11.61 +  add_deps (Syntax.init_pretty_global thy, NONE) a x y thy;
   11.62  
   11.63  fun specify_const decl thy =
   11.64    let val (t, thy') = Sign.declare_const_global decl thy;
   11.65 @@ -286,7 +285,7 @@
   11.66  
   11.67  local
   11.68  
   11.69 -fun check_def ctxt thy unchecked overloaded (b, tm) defs =
   11.70 +fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   11.71    let
   11.72      val name = Sign.full_name thy b;
   11.73      val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
   11.74 @@ -300,17 +299,17 @@
   11.75      val rhs_deps = rhs_consts @ rhs_types;
   11.76  
   11.77      val _ = check_overloading ctxt overloaded lhs_const;
   11.78 -  in defs |> dependencies ctxt unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   11.79 +  in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end
   11.80    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   11.81     [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
   11.82      Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
   11.83  
   11.84  in
   11.85  
   11.86 -fun add_def ctxt unchecked overloaded raw_axm thy =
   11.87 +fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy =
   11.88    let val axm = cert_axm ctxt raw_axm in
   11.89      thy
   11.90 -    |> map_defs (check_def ctxt thy unchecked overloaded axm)
   11.91 +    |> map_defs (check_def context thy unchecked overloaded axm)
   11.92      |> add_axiom ctxt axm
   11.93    end;
   11.94