removed proof data (see Pure/context.ML);
authorwenzelm
Wed Jun 22 19:41:28 2005 +0200 (2005-06-22)
changeset 16540e3d61eff7c12
parent 16539 60adb8b28377
child 16541 d539d47cce69
removed proof data (see Pure/context.ML);
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Jun 22 19:41:27 2005 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Jun 22 19:41:28 2005 +0200
     1.3 @@ -20,7 +20,6 @@
     1.4    val assumptions_of: context -> (cterm list * exporter) list
     1.5    val prems_of: context -> thm list
     1.6    val fact_index_of: context -> FactIndex.T
     1.7 -  val print_proof_data: theory -> unit
     1.8    val init: theory -> context
     1.9    val pretty_term: context -> term -> Pretty.T
    1.10    val pretty_typ: context -> typ -> Pretty.T
    1.11 @@ -150,163 +149,83 @@
    1.12    val pretty_context: context -> Pretty.T list
    1.13  end;
    1.14  
    1.15 -signature PRIVATE_PROOF_CONTEXT =
    1.16 -sig
    1.17 -  include PROOF_CONTEXT
    1.18 -  val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
    1.19 -    -> theory -> theory
    1.20 -  val print_data: Object.kind -> context -> unit
    1.21 -  val get_data: Object.kind -> (Object.T -> 'a) -> context -> 'a
    1.22 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
    1.23 -end;
    1.24 -
    1.25 -structure ProofContext: PRIVATE_PROOF_CONTEXT =
    1.26 +structure ProofContext: PROOF_CONTEXT =
    1.27  struct
    1.28  
    1.29 -
    1.30 -(** datatype context **)
    1.31 -
    1.32 -type exporter = bool -> cterm list -> thm -> thm Seq.seq;
    1.33 +(** generic proof contexts **)
    1.34  
    1.35 -datatype context =
    1.36 -  Context of
    1.37 -   {thy: theory,                                              (*current theory*)
    1.38 -    syntax: Syntax.syntax * string list * string list,        (*syntax with structs and mixfixed*)
    1.39 -    data: Object.T Symtab.table,                              (*user data*)
    1.40 -    asms:
    1.41 -      ((cterm list * exporter) list *                         (*assumes: A ==> _*)
    1.42 -        (string * thm list) list) *                           (*prems: A |- A *)
    1.43 -      (string * string) list,                                 (*fixes: !!x. _*)
    1.44 -    binds: (term * typ) Vartab.table,                         (*term bindings*)
    1.45 -    thms: NameSpace.naming *
    1.46 -      thm list NameSpace.table * FactIndex.T,                 (*local thms*)
    1.47 -    cases: (string * RuleCases.T) list,                       (*local contexts*)
    1.48 -    defs:
    1.49 -      typ Vartab.table *                                      (*type constraints*)
    1.50 -      sort Vartab.table *                                     (*default sorts*)
    1.51 -      string list *                                           (*used type variables*)
    1.52 -      term list Symtab.table};                                (*type variable occurrences*)
    1.53 -
    1.54 +type context = Context.proof;
    1.55  exception CONTEXT of string * context;
    1.56  
    1.57 -
    1.58 -fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) =
    1.59 -  Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds,
    1.60 -    thms = thms, cases = cases, defs = defs};
    1.61 -
    1.62 -fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) =
    1.63 -  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
    1.64 -
    1.65 -fun theory_of (Context {thy, ...}) = thy;
    1.66 +val theory_of = Context.theory_of_proof;
    1.67  val sign_of = theory_of;
    1.68 -fun syntax_of (Context {syntax, ...}) = syntax;
    1.69  
    1.70 -fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
    1.71 -val fixed_names_of = map #2 o fixes_of;
    1.72 -fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
    1.73 -fun is_known (ctxt as Context {defs = (types, _, _, _), ...}) x =
    1.74 -  is_some (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x;
    1.75 -fun type_occs (Context {defs = (_, _, _, tab), ...}) = tab;
    1.76 -
    1.77 -fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms;
    1.78 -fun prems_of (Context {asms = ((_, prems), _), ...}) = List.concat (map #2 prems);
    1.79 -fun fact_index_of (Context {thms = (_, _, idx), ...}) = idx;
    1.80 +val init = Context.init_proof;
    1.81  
    1.82  
    1.83  
    1.84 -(** user data **)
    1.85 -
    1.86 -(* errors *)
    1.87 -
    1.88 -fun of_theory thy = "\nof theory " ^ Context.str_of_thy thy;
    1.89 -
    1.90 -fun err_inconsistent kinds =
    1.91 -  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
    1.92 +(** Isar proof context information **)
    1.93  
    1.94 -fun err_dup_init thy kind =
    1.95 -  error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy);
    1.96 -
    1.97 -fun err_undef ctxt kind =
    1.98 -  raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt);
    1.99 -
   1.100 -fun err_uninit ctxt kind =
   1.101 -  raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^
   1.102 -    of_theory (theory_of ctxt), ctxt);
   1.103 +type exporter = bool -> cterm list -> thm -> thm Seq.seq;
   1.104  
   1.105 -fun err_access ctxt kind =
   1.106 -  raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^
   1.107 -    of_theory (theory_of ctxt), ctxt);
   1.108 +datatype ctxt =
   1.109 +  Ctxt of
   1.110 +   {syntax: Syntax.syntax * string list * string list,  (*syntax with structs and mixfixed*)
   1.111 +    asms:
   1.112 +      ((cterm list * exporter) list *                   (*assumes: A ==> _*)
   1.113 +        (string * thm list) list) *                     (*prems: A |- A *)
   1.114 +      (string * string) list,                           (*fixes: !!x. _*)
   1.115 +    binds: (term * typ) Vartab.table,                   (*term bindings*)
   1.116 +    thms: NameSpace.naming *                            (*local thms*)
   1.117 +      thm list NameSpace.table * FactIndex.T,
   1.118 +    cases: (string * RuleCases.T) list,                 (*local contexts*)
   1.119 +    defs:
   1.120 +      typ Vartab.table *                                (*type constraints*)
   1.121 +      sort Vartab.table *                               (*default sorts*)
   1.122 +      string list *                                     (*used type variables*)
   1.123 +      term list Symtab.table};                          (*type variable occurrences*)
   1.124  
   1.125 +fun make_ctxt (syntax, asms, binds, thms, cases, defs) =
   1.126 +  Ctxt {syntax = syntax, asms = asms, binds = binds, thms = thms, cases = cases, defs = defs};
   1.127  
   1.128 -(* data kind 'Isar/proof_data' *)
   1.129 -
   1.130 -structure ProofDataData = TheoryDataFun
   1.131 +structure ContextData = ProofDataFun
   1.132  (struct
   1.133 -  val name = "Isar/proof_data";
   1.134 -  type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
   1.135 -
   1.136 -  val empty = Symtab.empty;
   1.137 -  val copy = I;
   1.138 -  val extend = I;
   1.139 -  fun merge _ tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
   1.140 -    handle Symtab.DUPS kinds => err_inconsistent kinds;
   1.141 -  fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
   1.142 +  val name = "Isar/context";
   1.143 +  type T = ctxt;
   1.144 +  fun init thy =
   1.145 +    make_ctxt ((Sign.syn_of thy, [], []), (([], []), []), Vartab.empty,
   1.146 +      (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
   1.147 +      (Vartab.empty, Vartab.empty, [], Symtab.empty));
   1.148 +  fun print _ _ = ();
   1.149  end);
   1.150  
   1.151 -val _ = Context.add_setup [ProofDataData.init];
   1.152 -val print_proof_data = ProofDataData.print;
   1.153 +val _ = Context.add_setup [ContextData.init];
   1.154  
   1.155 +fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
   1.156  
   1.157 -(* init proof data *)
   1.158 +fun map_context f = ContextData.map (fn Ctxt {syntax, asms, binds, thms, cases, defs} =>
   1.159 +  make_ctxt (f (syntax, asms, binds, thms, cases, defs)));
   1.160  
   1.161 -fun init_data kind meths thy =
   1.162 -  let
   1.163 -    val name = Object.name_of_kind kind;
   1.164 -    val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy)
   1.165 -      handle Symtab.DUP _ => err_dup_init thy name;
   1.166 -  in thy |> ProofDataData.put tab end;
   1.167 +val syntax_of = #syntax o rep_context;
   1.168  
   1.169 -
   1.170 -(* access data *)
   1.171 +val assumptions_of = #1 o #1 o #asms o rep_context;
   1.172 +val prems_of = List.concat o map #2 o #2 o #1 o #asms o rep_context;
   1.173 +val fixes_of = #2 o #asms o rep_context;
   1.174 +val fixed_names_of = map #2 o fixes_of;
   1.175  
   1.176 -fun lookup_data (ctxt as Context {data, ...}) kind =
   1.177 -  let
   1.178 -    val thy = theory_of ctxt;
   1.179 -    val name = Object.name_of_kind kind;
   1.180 -  in
   1.181 -    (case Symtab.lookup (ProofDataData.get thy, name) of
   1.182 -      SOME (k, meths) =>
   1.183 -        if Object.eq_kind (kind, k) then
   1.184 -          (case Symtab.lookup (data, name) of
   1.185 -            SOME x => (x, meths)
   1.186 -          | NONE => err_undef ctxt name)
   1.187 -        else err_access ctxt name
   1.188 -    | NONE => err_uninit ctxt name)
   1.189 -  end;
   1.190 +val binds_of =  #binds o rep_context;
   1.191  
   1.192 -fun get_data kind f ctxt =
   1.193 -  let val (x, _) = lookup_data ctxt kind
   1.194 -  in f x handle Match => Object.kind_error kind end;
   1.195 +val thms_of = #thms o rep_context;
   1.196 +val fact_index_of = #3 o thms_of;
   1.197 +
   1.198 +val cases_of = #cases o rep_context;
   1.199  
   1.200 -fun print_data kind ctxt =
   1.201 -  let val (x, (_, prt)) = lookup_data ctxt kind
   1.202 -  in prt ctxt x end;
   1.203 -
   1.204 -fun put_data kind f x ctxt =
   1.205 - (lookup_data ctxt kind;
   1.206 -  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   1.207 -    (thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data),
   1.208 -      asms, binds, thms, cases, defs)) ctxt);
   1.209 +val defaults_of = #defs o rep_context;
   1.210 +val type_occs_of = #4 o defaults_of;
   1.211  
   1.212 -
   1.213 -(* init context *)
   1.214 -
   1.215 -fun init thy =
   1.216 -  let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
   1.217 -    make_context (thy, (Sign.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
   1.218 -      (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
   1.219 -      (Vartab.empty, Vartab.empty, [], Symtab.empty))
   1.220 -  end;
   1.221 +fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
   1.222 +fun is_known ctxt x =
   1.223 +  is_some (Vartab.lookup (#1 (defaults_of ctxt), (x, ~1))) orelse is_fixed ctxt x;
   1.224  
   1.225  
   1.226  
   1.227 @@ -360,10 +279,10 @@
   1.228  
   1.229  in
   1.230  
   1.231 -fun add_syntax decls =
   1.232 -  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
   1.233 +fun add_syntax decls ctxt = ctxt |>
   1.234 +  map_context (fn ((syn, structs, mixfixed), asms, binds, thms, cases, defs) =>
   1.235      let
   1.236 -      val is_logtype = Sign.is_logtype thy;
   1.237 +      val is_logtype = Sign.is_logtype (theory_of ctxt);
   1.238        val structs' = structs @ List.mapPartial prep_struct decls;
   1.239        val mxs = List.mapPartial prep_mixfix decls;
   1.240        val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
   1.241 @@ -372,10 +291,12 @@
   1.242          |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
   1.243          |> Syntax.extend_const_gram is_logtype ("", true) mxs
   1.244          |> Syntax.extend_trfuns ([], mk trs, [], []);
   1.245 -    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end);
   1.246 +    in ((syn', structs', fixed @ mixfixed), asms, binds, thms, cases, defs) end);
   1.247  
   1.248 -fun syn_of (Context {syntax = (syn, structs, _), ...}) =
   1.249 -  let val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs
   1.250 +fun syn_of ctxt =
   1.251 +  let
   1.252 +    val (syn, structs, _) = syntax_of ctxt;
   1.253 +    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
   1.254    in syn |> Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs') end;
   1.255  
   1.256  end;
   1.257 @@ -413,17 +334,19 @@
   1.258  
   1.259  (** default sorts and types **)
   1.260  
   1.261 -fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi);
   1.262 +fun def_sort ctxt xi = Vartab.lookup (#2 (defaults_of ctxt), xi);
   1.263  
   1.264 -fun def_type (Context {binds, defs = (types, _, _, _), ...}) pattern xi =
   1.265 -  (case Vartab.lookup (types, xi) of
   1.266 -    NONE =>
   1.267 -      if pattern then NONE
   1.268 -      else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
   1.269 -  | some => some);
   1.270 +fun def_type ctxt pattern xi =
   1.271 +  let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in
   1.272 +    (case Vartab.lookup (types, xi) of
   1.273 +      NONE =>
   1.274 +        if pattern then NONE
   1.275 +        else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
   1.276 +    | some => some)
   1.277 +  end;
   1.278  
   1.279 -fun default_type (Context {defs = (types, _, _, _), ...}) x = Vartab.lookup (types, (x, ~1));
   1.280 -fun used_types (Context {defs = (_, _, used, _), ...}) = used;
   1.281 +fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt), (x, ~1));
   1.282 +val used_types = #3 o defaults_of;
   1.283  
   1.284  
   1.285  
   1.286 @@ -532,11 +455,12 @@
   1.287    let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
   1.288    in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
   1.289  
   1.290 -fun norm_term (ctxt as Context {binds, ...}) schematic =
   1.291 +fun norm_term ctxt schematic =
   1.292    let
   1.293      (*raised when norm has no effect on a term, to do sharing instead of copying*)
   1.294      exception SAME;
   1.295  
   1.296 +    val binds = binds_of ctxt;
   1.297      fun norm (t as Var (xi, T)) =
   1.298            (case Vartab.lookup (binds, xi) of
   1.299              SOME (u, U) =>
   1.300 @@ -664,8 +588,8 @@
   1.301        SOME T => Vartab.update (((x, ~1), T), types)
   1.302      | NONE => types));
   1.303  
   1.304 -fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   1.305 -  (thy, syntax, data, asms, binds, thms, cases, f defs));
   1.306 +fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   1.307 +  (syntax, asms, binds, thms, cases, f defs));
   1.308  
   1.309  in
   1.310  
   1.311 @@ -675,12 +599,13 @@
   1.312    |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ))
   1.313    |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ));
   1.314  
   1.315 -fun declare_term t (ctxt as Context {asms = (_, fixes), ...}) =
   1.316 +fun declare_term t ctxt =
   1.317    ctxt
   1.318    |> declare_term_syntax t
   1.319    |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
   1.320    |> map_defaults (fn (types, sorts, used, occ) =>
   1.321 -      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ));
   1.322 +      (ins_skolem (fn x =>
   1.323 +        Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
   1.324  
   1.325  end;
   1.326  
   1.327 @@ -703,16 +628,14 @@
   1.328  
   1.329  (* warn_extra_tfrees *)
   1.330  
   1.331 -fun warn_extra_tfrees
   1.332 -    (ctxt1 as Context {defs = (_, _, _, occ1), ...})
   1.333 -    (ctxt2 as Context {defs = (_, _, _, occ2), ...}) =
   1.334 +fun warn_extra_tfrees ctxt1 ctxt2 =
   1.335    let
   1.336      fun known_tfree a (Type (_, Ts)) = exists (known_tfree a) Ts
   1.337        | known_tfree a (TFree (a', _)) = a = a'
   1.338        | known_tfree _ _ = false;
   1.339  
   1.340      val extras =
   1.341 -      Library.gen_rems Library.eq_fst (Symtab.dest occ2, Symtab.dest occ1)
   1.342 +      Library.gen_rems Library.eq_fst (pairself (Symtab.dest o type_occs_of) (ctxt1, ctxt2))
   1.343        |> map (fn (a, ts) => map (pair a) (List.mapPartial (try (#1 o Term.dest_Free)) ts))
   1.344        |> List.concat
   1.345        |> List.mapPartial (fn (a, x) =>
   1.346 @@ -735,8 +658,8 @@
   1.347      val extra_fixes = fixed_names_of inner \\ fixed_names_of outer;
   1.348      fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes)
   1.349        | still_fixed _ = false;
   1.350 -    val occs_inner = type_occs inner;
   1.351 -    val occs_outer = type_occs outer;
   1.352 +    val occs_inner = type_occs_of inner;
   1.353 +    val occs_outer = type_occs_of outer;
   1.354      fun add a gen =
   1.355        if is_some (Symtab.lookup (occs_outer, a)) orelse
   1.356          exists still_fixed (Symtab.lookup_multi (occs_inner, a))
   1.357 @@ -814,8 +737,8 @@
   1.358  
   1.359  local
   1.360  
   1.361 -fun del_bind xi = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   1.362 -  (thy, syntax, data, asms, Vartab.delete_safe xi binds, thms, cases, defs));
   1.363 +fun del_bind xi = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   1.364 +  (syntax, asms, Vartab.delete_safe xi binds, thms, cases, defs));
   1.365  
   1.366  fun upd_bind ((x, i), t) =
   1.367    let
   1.368 @@ -824,8 +747,8 @@
   1.369        if null (Term.term_tvars t \\ Term.typ_tvars T) then t
   1.370        else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   1.371    in
   1.372 -    map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   1.373 -      (thy, syntax, data, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
   1.374 +    map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   1.375 +      (syntax, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
   1.376      o declare_term t'
   1.377    end;
   1.378  
   1.379 @@ -971,17 +894,20 @@
   1.380  (* get_thm(s) *)
   1.381  
   1.382  (*beware of proper order of evaluation!*)
   1.383 -fun retrieve_thms from_thy pick (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
   1.384 -  let val thy_ref = Theory.self_ref thy in
   1.385 +fun retrieve_thms from_thy pick ctxt =
   1.386 +  let
   1.387 +    val thy_ref = Theory.self_ref (theory_of ctxt);
   1.388 +    val (_, (space, tab), _) = thms_of ctxt;
   1.389 +  in
   1.390      fn xthmref =>
   1.391        let
   1.392 +        val thy = Theory.deref thy_ref;
   1.393          val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
   1.394          val name = PureThy.name_of_thmref thmref;
   1.395 -        val thy' = Theory.deref thy_ref;
   1.396        in
   1.397          (case Symtab.lookup (tab, name) of
   1.398 -          SOME ths => map (Thm.transfer thy') (PureThy.select_thm thmref ths)
   1.399 -        | NONE => from_thy thy' xthmref) |> pick name
   1.400 +          SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
   1.401 +        | NONE => from_thy thy xthmref) |> pick name
   1.402        end
   1.403    end;
   1.404  
   1.405 @@ -1009,20 +935,20 @@
   1.406  
   1.407  (* name space operations *)
   1.408  
   1.409 -fun extern_thm (Context {thms = (_, (space, _), _), ...}) = NameSpace.extern space;
   1.410 +val extern_thm = NameSpace.extern o #1 o #2 o thms_of;
   1.411  
   1.412 -fun map_naming f = map_context (fn (thy, syntax, data, asms, binds,
   1.413 +fun map_naming f = map_context (fn (syntax, asms, binds,
   1.414      (naming, table, index), cases, defs) =>
   1.415 -  (thy, syntax, data, asms, binds, (f naming, table, index), cases, defs));
   1.416 +  (syntax, asms, binds, (f naming, table, index), cases, defs));
   1.417  
   1.418  val qualified_names = map_naming NameSpace.qualified_names;
   1.419  val no_base_names = map_naming NameSpace.no_base_names;
   1.420  val custom_accesses = map_naming o NameSpace.custom_accesses;
   1.421 -fun restore_naming (Context {thms, ...}) = map_naming (K (#1 thms));
   1.422 +val restore_naming = map_naming o K o #1 o thms_of;
   1.423  
   1.424  fun hide_thms fully names = map_context
   1.425 -  (fn (thy, syntax, data, asms, binds, (naming, (space, tab), index), cases, defs) =>
   1.426 -    (thy, syntax, data, asms, binds,
   1.427 +  (fn (syntax, asms, binds, (naming, (space, tab), index), cases, defs) =>
   1.428 +    (syntax, asms, binds,
   1.429        (naming, (fold (NameSpace.hide fully) names space, tab), index), cases, defs));
   1.430  
   1.431  
   1.432 @@ -1030,13 +956,13 @@
   1.433  
   1.434  fun put_thms ("", _) ctxt = ctxt
   1.435    | put_thms (bname, ths) ctxt = ctxt |> map_context
   1.436 -      (fn (thy, syntax, data, asms, binds, (naming, (space, tab), index), cases, defs) =>
   1.437 +      (fn (syntax, asms, binds, (naming, (space, tab), index), cases, defs) =>
   1.438          let
   1.439            val name = NameSpace.full naming bname;
   1.440            val space' = NameSpace.declare naming name space;
   1.441            val tab' = Symtab.update ((name, ths), tab);
   1.442            val index' = FactIndex.add (is_known ctxt) (name, ths) index;
   1.443 -        in (thy, syntax, data, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
   1.444 +        in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
   1.445  
   1.446  fun put_thm (name, th) = put_thms (name, [th]);
   1.447  val put_thmss = fold put_thms;
   1.448 @@ -1044,10 +970,9 @@
   1.449  
   1.450  (* reset_thms *)
   1.451  
   1.452 -fun reset_thms name =    (* FIXME hide!? *)
   1.453 -  map_context (fn (thy, syntax, data, asms, binds, (q, (space, tab), index), cases, defs) =>
   1.454 -    (thy, syntax, data, asms, binds, (q, (space, Symtab.delete_safe name tab), index),
   1.455 -      cases, defs));
   1.456 +fun reset_thms name =    (* FIXME NameSpace.hide!? *)
   1.457 +  map_context (fn (syntax, asms, binds, (q, (space, tab), index), cases, defs) =>
   1.458 +    (syntax, asms, binds, (q, (space, Symtab.delete_safe name tab), index), cases, defs));
   1.459  
   1.460  
   1.461  (* note_thmss *)
   1.462 @@ -1150,8 +1075,8 @@
   1.463      val asmss = map #2 results;
   1.464      val thmss = map #3 results;
   1.465      val ctxt3 = ctxt2 |> map_context
   1.466 -      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
   1.467 -        (thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
   1.468 +      (fn (syntax, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
   1.469 +        (syntax, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
   1.470            cases, defs));
   1.471      val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3);
   1.472    in (warn_extra_tfrees ctxt ctxt4, thmss) end;
   1.473 @@ -1198,8 +1123,8 @@
   1.474  local
   1.475  
   1.476  fun map_fixes f =
   1.477 -  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs) =>
   1.478 -    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs));
   1.479 +  map_context (fn (syntax, (assumes, fixes), binds, thms, cases, defs) =>
   1.480 +    (syntax, (assumes, f fixes), binds, thms, cases, defs));
   1.481  
   1.482  fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
   1.483  
   1.484 @@ -1303,13 +1228,13 @@
   1.485  
   1.486  in
   1.487  
   1.488 -fun get_case (ctxt as Context {cases, ...}) name xs =
   1.489 -  (case assoc (cases, name) of
   1.490 +fun get_case ctxt name xs =
   1.491 +  (case assoc_string (cases_of ctxt, name) of
   1.492      NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
   1.493    | SOME c => prep_case ctxt name xs c);
   1.494  
   1.495 -fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
   1.496 -  (thy, syntax, data, asms, binds, thms, fold add_case xs cases, defs));
   1.497 +fun add_cases xs = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
   1.498 +  (syntax, asms, binds, thms, fold add_case xs cases, defs));
   1.499  
   1.500  end;
   1.501  
   1.502 @@ -1340,8 +1265,9 @@
   1.503  
   1.504  (* term bindings *)
   1.505  
   1.506 -fun pretty_binds (ctxt as Context {binds, ...}) =
   1.507 +fun pretty_binds ctxt =
   1.508    let
   1.509 +    val binds = binds_of ctxt;
   1.510      fun prt_bind (xi, (t, T)) = pretty_term ctxt (Logic.mk_equals (Var (xi, T), t));
   1.511    in
   1.512      if Vartab.is_empty binds andalso not (! verbose) then []
   1.513 @@ -1353,15 +1279,15 @@
   1.514  
   1.515  (* local theorems *)
   1.516  
   1.517 -fun pretty_lthms (ctxt as Context {thms = (_, table, _), ...}) =
   1.518 -  pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table table);
   1.519 +fun pretty_lthms ctxt =
   1.520 +  pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#2 (thms_of ctxt)));
   1.521  
   1.522  val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
   1.523  
   1.524  
   1.525  (* local contexts *)
   1.526  
   1.527 -fun pretty_cases (ctxt as Context {cases, ...}) =
   1.528 +fun pretty_cases ctxt =
   1.529    let
   1.530      val prt_term = pretty_term ctxt;
   1.531  
   1.532 @@ -1383,6 +1309,8 @@
   1.533            (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
   1.534          (if forall (null o #2) asms then []
   1.535            else prt_sect "assume" [Pretty.str "and"] prt_asm asms)));
   1.536 +
   1.537 +    val cases = cases_of ctxt;
   1.538    in
   1.539      if null cases andalso not (! verbose) then []
   1.540      else [Pretty.big_list "cases:"
   1.541 @@ -1429,7 +1357,7 @@
   1.542  
   1.543  (* main context *)
   1.544  
   1.545 -fun pretty_context (ctxt as Context {cases, defs = (types, sorts, used, _), ...}) =
   1.546 +fun pretty_context ctxt =
   1.547    let
   1.548      val prt_term = pretty_term ctxt;
   1.549      val prt_typ = pretty_typ ctxt;
   1.550 @@ -1451,6 +1379,8 @@
   1.551  
   1.552      val prt_defT = prt_atom prt_var prt_typ;
   1.553      val prt_defS = prt_atom prt_varT prt_sort;
   1.554 +
   1.555 +    val (types, sorts, used, _) = defaults_of ctxt;
   1.556    in
   1.557      verb_single (K pretty_thy) @
   1.558      pretty_asms ctxt @