# HG changeset patch
# User wenzelm
# Date 1119462088 -7200
# Node ID e3d61eff7c12c08e8281ca8970beffd2f9e2c3d4
# Parent  60adb8b28377ef5b3b0d010cc008a2a13c101468
removed proof data (see Pure/context.ML);

diff -r 60adb8b28377 -r e3d61eff7c12 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Jun 22 19:41:27 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Jun 22 19:41:28 2005 +0200
@@ -20,7 +20,6 @@
   val assumptions_of: context -> (cterm list * exporter) list
   val prems_of: context -> thm list
   val fact_index_of: context -> FactIndex.T
-  val print_proof_data: theory -> unit
   val init: theory -> context
   val pretty_term: context -> term -> Pretty.T
   val pretty_typ: context -> typ -> Pretty.T
@@ -150,163 +149,83 @@
   val pretty_context: context -> Pretty.T list
 end;
 
-signature PRIVATE_PROOF_CONTEXT =
-sig
-  include PROOF_CONTEXT
-  val init_data: Object.kind -> (theory -> Object.T) * (context -> Object.T -> unit)
-    -> theory -> theory
-  val print_data: Object.kind -> context -> unit
-  val get_data: Object.kind -> (Object.T -> 'a) -> context -> 'a
-  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> context -> context
-end;
-
-structure ProofContext: PRIVATE_PROOF_CONTEXT =
+structure ProofContext: PROOF_CONTEXT =
 struct
 
-
-(** datatype context **)
-
-type exporter = bool -> cterm list -> thm -> thm Seq.seq;
+(** generic proof contexts **)
 
-datatype context =
-  Context of
-   {thy: theory,                                              (*current theory*)
-    syntax: Syntax.syntax * string list * string list,        (*syntax with structs and mixfixed*)
-    data: Object.T Symtab.table,                              (*user data*)
-    asms:
-      ((cterm list * exporter) list *                         (*assumes: A ==> _*)
-        (string * thm list) list) *                           (*prems: A |- A *)
-      (string * string) list,                                 (*fixes: !!x. _*)
-    binds: (term * typ) Vartab.table,                         (*term bindings*)
-    thms: NameSpace.naming *
-      thm list NameSpace.table * FactIndex.T,                 (*local thms*)
-    cases: (string * RuleCases.T) list,                       (*local contexts*)
-    defs:
-      typ Vartab.table *                                      (*type constraints*)
-      sort Vartab.table *                                     (*default sorts*)
-      string list *                                           (*used type variables*)
-      term list Symtab.table};                                (*type variable occurrences*)
-
+type context = Context.proof;
 exception CONTEXT of string * context;
 
-
-fun make_context (thy, syntax, data, asms, binds, thms, cases, defs) =
-  Context {thy = thy, syntax = syntax, data = data, asms = asms, binds = binds,
-    thms = thms, cases = cases, defs = defs};
-
-fun map_context f (Context {thy, syntax, data, asms, binds, thms, cases, defs}) =
-  make_context (f (thy, syntax, data, asms, binds, thms, cases, defs));
-
-fun theory_of (Context {thy, ...}) = thy;
+val theory_of = Context.theory_of_proof;
 val sign_of = theory_of;
-fun syntax_of (Context {syntax, ...}) = syntax;
 
-fun fixes_of (Context {asms = (_, fixes), ...}) = fixes;
-val fixed_names_of = map #2 o fixes_of;
-fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
-fun is_known (ctxt as Context {defs = (types, _, _, _), ...}) x =
-  is_some (Vartab.lookup (types, (x, ~1))) orelse is_fixed ctxt x;
-fun type_occs (Context {defs = (_, _, _, tab), ...}) = tab;
-
-fun assumptions_of (Context {asms = ((asms, _), _), ...}) = asms;
-fun prems_of (Context {asms = ((_, prems), _), ...}) = List.concat (map #2 prems);
-fun fact_index_of (Context {thms = (_, _, idx), ...}) = idx;
+val init = Context.init_proof;
 
 
 
-(** user data **)
-
-(* errors *)
-
-fun of_theory thy = "\nof theory " ^ Context.str_of_thy thy;
-
-fun err_inconsistent kinds =
-  error ("Attempt to merge different versions of " ^ commas_quote kinds ^ " proof data");
+(** Isar proof context information **)
 
-fun err_dup_init thy kind =
-  error ("Duplicate initialization of " ^ quote kind ^ " proof data" ^ of_theory thy);
-
-fun err_undef ctxt kind =
-  raise CONTEXT ("Tried to access undefined " ^ quote kind ^ " proof data", ctxt);
-
-fun err_uninit ctxt kind =
-  raise CONTEXT ("Tried to access uninitialized " ^ quote kind ^ " proof data" ^
-    of_theory (theory_of ctxt), ctxt);
+type exporter = bool -> cterm list -> thm -> thm Seq.seq;
 
-fun err_access ctxt kind =
-  raise CONTEXT ("Unauthorized access to " ^ quote kind ^ " proof data" ^
-    of_theory (theory_of ctxt), ctxt);
+datatype ctxt =
+  Ctxt of
+   {syntax: Syntax.syntax * string list * string list,  (*syntax with structs and mixfixed*)
+    asms:
+      ((cterm list * exporter) list *                   (*assumes: A ==> _*)
+        (string * thm list) list) *                     (*prems: A |- A *)
+      (string * string) list,                           (*fixes: !!x. _*)
+    binds: (term * typ) Vartab.table,                   (*term bindings*)
+    thms: NameSpace.naming *                            (*local thms*)
+      thm list NameSpace.table * FactIndex.T,
+    cases: (string * RuleCases.T) list,                 (*local contexts*)
+    defs:
+      typ Vartab.table *                                (*type constraints*)
+      sort Vartab.table *                               (*default sorts*)
+      string list *                                     (*used type variables*)
+      term list Symtab.table};                          (*type variable occurrences*)
 
+fun make_ctxt (syntax, asms, binds, thms, cases, defs) =
+  Ctxt {syntax = syntax, asms = asms, binds = binds, thms = thms, cases = cases, defs = defs};
 
-(* data kind 'Isar/proof_data' *)
-
-structure ProofDataData = TheoryDataFun
+structure ContextData = ProofDataFun
 (struct
-  val name = "Isar/proof_data";
-  type T = (Object.kind * ((theory -> Object.T) * (context -> Object.T -> unit))) Symtab.table;
-
-  val empty = Symtab.empty;
-  val copy = I;
-  val extend = I;
-  fun merge _ tabs = Symtab.merge (Object.eq_kind o pairself fst) tabs
-    handle Symtab.DUPS kinds => err_inconsistent kinds;
-  fun print _ tab = Pretty.writeln (Pretty.strs (map #1 (Symtab.dest tab)));
+  val name = "Isar/context";
+  type T = ctxt;
+  fun init thy =
+    make_ctxt ((Sign.syn_of thy, [], []), (([], []), []), Vartab.empty,
+      (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
+      (Vartab.empty, Vartab.empty, [], Symtab.empty));
+  fun print _ _ = ();
 end);
 
-val _ = Context.add_setup [ProofDataData.init];
-val print_proof_data = ProofDataData.print;
+val _ = Context.add_setup [ContextData.init];
 
+fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
 
-(* init proof data *)
+fun map_context f = ContextData.map (fn Ctxt {syntax, asms, binds, thms, cases, defs} =>
+  make_ctxt (f (syntax, asms, binds, thms, cases, defs)));
 
-fun init_data kind meths thy =
-  let
-    val name = Object.name_of_kind kind;
-    val tab = Symtab.update_new ((name, (kind, meths)), ProofDataData.get thy)
-      handle Symtab.DUP _ => err_dup_init thy name;
-  in thy |> ProofDataData.put tab end;
+val syntax_of = #syntax o rep_context;
 
-
-(* access data *)
+val assumptions_of = #1 o #1 o #asms o rep_context;
+val prems_of = List.concat o map #2 o #2 o #1 o #asms o rep_context;
+val fixes_of = #2 o #asms o rep_context;
+val fixed_names_of = map #2 o fixes_of;
 
-fun lookup_data (ctxt as Context {data, ...}) kind =
-  let
-    val thy = theory_of ctxt;
-    val name = Object.name_of_kind kind;
-  in
-    (case Symtab.lookup (ProofDataData.get thy, name) of
-      SOME (k, meths) =>
-        if Object.eq_kind (kind, k) then
-          (case Symtab.lookup (data, name) of
-            SOME x => (x, meths)
-          | NONE => err_undef ctxt name)
-        else err_access ctxt name
-    | NONE => err_uninit ctxt name)
-  end;
+val binds_of =  #binds o rep_context;
 
-fun get_data kind f ctxt =
-  let val (x, _) = lookup_data ctxt kind
-  in f x handle Match => Object.kind_error kind end;
+val thms_of = #thms o rep_context;
+val fact_index_of = #3 o thms_of;
+
+val cases_of = #cases o rep_context;
 
-fun print_data kind ctxt =
-  let val (x, (_, prt)) = lookup_data ctxt kind
-  in prt ctxt x end;
-
-fun put_data kind f x ctxt =
- (lookup_data ctxt kind;
-  map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-    (thy, syntax, Symtab.update ((Object.name_of_kind kind, f x), data),
-      asms, binds, thms, cases, defs)) ctxt);
+val defaults_of = #defs o rep_context;
+val type_occs_of = #4 o defaults_of;
 
-
-(* init context *)
-
-fun init thy =
-  let val data = Symtab.map (fn (_, (f, _)) => f thy) (ProofDataData.get thy) in
-    make_context (thy, (Sign.syn_of thy, [], []), data, (([], []), []), Vartab.empty,
-      (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [],
-      (Vartab.empty, Vartab.empty, [], Symtab.empty))
-  end;
+fun is_fixed ctxt x = exists (equal x o #2) (fixes_of ctxt);
+fun is_known ctxt x =
+  is_some (Vartab.lookup (#1 (defaults_of ctxt), (x, ~1))) orelse is_fixed ctxt x;
 
 
 
@@ -360,10 +279,10 @@
 
 in
 
-fun add_syntax decls =
-  map_context (fn (thy, (syn, structs, mixfixed), data, asms, binds, thms, cases, defs) =>
+fun add_syntax decls ctxt = ctxt |>
+  map_context (fn ((syn, structs, mixfixed), asms, binds, thms, cases, defs) =>
     let
-      val is_logtype = Sign.is_logtype thy;
+      val is_logtype = Sign.is_logtype (theory_of ctxt);
       val structs' = structs @ List.mapPartial prep_struct decls;
       val mxs = List.mapPartial prep_mixfix decls;
       val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls);
@@ -372,10 +291,12 @@
         |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
         |> Syntax.extend_const_gram is_logtype ("", true) mxs
         |> Syntax.extend_trfuns ([], mk trs, [], []);
-    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end);
+    in ((syn', structs', fixed @ mixfixed), asms, binds, thms, cases, defs) end);
 
-fun syn_of (Context {syntax = (syn, structs, _), ...}) =
-  let val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs
+fun syn_of ctxt =
+  let
+    val (syn, structs, _) = syntax_of ctxt;
+    val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs;
   in syn |> Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs') end;
 
 end;
@@ -413,17 +334,19 @@
 
 (** default sorts and types **)
 
-fun def_sort (Context {defs = (_, sorts, _, _), ...}) xi = Vartab.lookup (sorts, xi);
+fun def_sort ctxt xi = Vartab.lookup (#2 (defaults_of ctxt), xi);
 
-fun def_type (Context {binds, defs = (types, _, _, _), ...}) pattern xi =
-  (case Vartab.lookup (types, xi) of
-    NONE =>
-      if pattern then NONE
-      else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
-  | some => some);
+fun def_type ctxt pattern xi =
+  let val {binds, defs = (types, _, _, _), ...} = rep_context ctxt in
+    (case Vartab.lookup (types, xi) of
+      NONE =>
+        if pattern then NONE
+        else Vartab.lookup (binds, xi) |> Option.map (TypeInfer.polymorphicT o #2)
+    | some => some)
+  end;
 
-fun default_type (Context {defs = (types, _, _, _), ...}) x = Vartab.lookup (types, (x, ~1));
-fun used_types (Context {defs = (_, _, used, _), ...}) = used;
+fun default_type ctxt x = Vartab.lookup (#1 (defaults_of ctxt), (x, ~1));
+val used_types = #3 o defaults_of;
 
 
 
@@ -532,11 +455,12 @@
   let val maxidx = Int.max (Term.maxidx_of_typ T, Term.maxidx_of_typ U)
   in #1 (Type.unify (Sign.tsig_of (theory_of ctxt)) (Vartab.empty, maxidx) (T, U)) end;
 
-fun norm_term (ctxt as Context {binds, ...}) schematic =
+fun norm_term ctxt schematic =
   let
     (*raised when norm has no effect on a term, to do sharing instead of copying*)
     exception SAME;
 
+    val binds = binds_of ctxt;
     fun norm (t as Var (xi, T)) =
           (case Vartab.lookup (binds, xi) of
             SOME (u, U) =>
@@ -664,8 +588,8 @@
       SOME T => Vartab.update (((x, ~1), T), types)
     | NONE => types));
 
-fun map_defaults f = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-  (thy, syntax, data, asms, binds, thms, cases, f defs));
+fun map_defaults f = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
+  (syntax, asms, binds, thms, cases, f defs));
 
 in
 
@@ -675,12 +599,13 @@
   |> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts (sorts, t), used, occ))
   |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used (used, t), occ));
 
-fun declare_term t (ctxt as Context {asms = (_, fixes), ...}) =
+fun declare_term t ctxt =
   ctxt
   |> declare_term_syntax t
   |> map_defaults (fn (types, sorts, used, occ) => (types, sorts, used, ins_occs (occ, t)))
   |> map_defaults (fn (types, sorts, used, occ) =>
-      (ins_skolem (fn x => Vartab.lookup (types, (x, ~1))) types fixes, sorts, used, occ));
+      (ins_skolem (fn x =>
+        Vartab.lookup (types, (x, ~1))) types (fixes_of ctxt), sorts, used, occ));
 
 end;
 
@@ -703,16 +628,14 @@
 
 (* warn_extra_tfrees *)
 
-fun warn_extra_tfrees
-    (ctxt1 as Context {defs = (_, _, _, occ1), ...})
-    (ctxt2 as Context {defs = (_, _, _, occ2), ...}) =
+fun warn_extra_tfrees ctxt1 ctxt2 =
   let
     fun known_tfree a (Type (_, Ts)) = exists (known_tfree a) Ts
       | known_tfree a (TFree (a', _)) = a = a'
       | known_tfree _ _ = false;
 
     val extras =
-      Library.gen_rems Library.eq_fst (Symtab.dest occ2, Symtab.dest occ1)
+      Library.gen_rems Library.eq_fst (pairself (Symtab.dest o type_occs_of) (ctxt1, ctxt2))
       |> map (fn (a, ts) => map (pair a) (List.mapPartial (try (#1 o Term.dest_Free)) ts))
       |> List.concat
       |> List.mapPartial (fn (a, x) =>
@@ -735,8 +658,8 @@
     val extra_fixes = fixed_names_of inner \\ fixed_names_of outer;
     fun still_fixed (Free (x, _)) = not (x mem_string extra_fixes)
       | still_fixed _ = false;
-    val occs_inner = type_occs inner;
-    val occs_outer = type_occs outer;
+    val occs_inner = type_occs_of inner;
+    val occs_outer = type_occs_of outer;
     fun add a gen =
       if is_some (Symtab.lookup (occs_outer, a)) orelse
         exists still_fixed (Symtab.lookup_multi (occs_inner, a))
@@ -814,8 +737,8 @@
 
 local
 
-fun del_bind xi = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-  (thy, syntax, data, asms, Vartab.delete_safe xi binds, thms, cases, defs));
+fun del_bind xi = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
+  (syntax, asms, Vartab.delete_safe xi binds, thms, cases, defs));
 
 fun upd_bind ((x, i), t) =
   let
@@ -824,8 +747,8 @@
       if null (Term.term_tvars t \\ Term.typ_tvars T) then t
       else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T);
   in
-    map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-      (thy, syntax, data, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
+    map_context (fn (syntax, asms, binds, thms, cases, defs) =>
+      (syntax, asms, Vartab.update (((x, i), (t', T)), binds), thms, cases, defs))
     o declare_term t'
   end;
 
@@ -971,17 +894,20 @@
 (* get_thm(s) *)
 
 (*beware of proper order of evaluation!*)
-fun retrieve_thms from_thy pick (ctxt as Context {thy, thms = (_, (space, tab), _), ...}) =
-  let val thy_ref = Theory.self_ref thy in
+fun retrieve_thms from_thy pick ctxt =
+  let
+    val thy_ref = Theory.self_ref (theory_of ctxt);
+    val (_, (space, tab), _) = thms_of ctxt;
+  in
     fn xthmref =>
       let
+        val thy = Theory.deref thy_ref;
         val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref;
         val name = PureThy.name_of_thmref thmref;
-        val thy' = Theory.deref thy_ref;
       in
         (case Symtab.lookup (tab, name) of
-          SOME ths => map (Thm.transfer thy') (PureThy.select_thm thmref ths)
-        | NONE => from_thy thy' xthmref) |> pick name
+          SOME ths => map (Thm.transfer thy) (PureThy.select_thm thmref ths)
+        | NONE => from_thy thy xthmref) |> pick name
       end
   end;
 
@@ -1009,20 +935,20 @@
 
 (* name space operations *)
 
-fun extern_thm (Context {thms = (_, (space, _), _), ...}) = NameSpace.extern space;
+val extern_thm = NameSpace.extern o #1 o #2 o thms_of;
 
-fun map_naming f = map_context (fn (thy, syntax, data, asms, binds,
+fun map_naming f = map_context (fn (syntax, asms, binds,
     (naming, table, index), cases, defs) =>
-  (thy, syntax, data, asms, binds, (f naming, table, index), cases, defs));
+  (syntax, asms, binds, (f naming, table, index), cases, defs));
 
 val qualified_names = map_naming NameSpace.qualified_names;
 val no_base_names = map_naming NameSpace.no_base_names;
 val custom_accesses = map_naming o NameSpace.custom_accesses;
-fun restore_naming (Context {thms, ...}) = map_naming (K (#1 thms));
+val restore_naming = map_naming o K o #1 o thms_of;
 
 fun hide_thms fully names = map_context
-  (fn (thy, syntax, data, asms, binds, (naming, (space, tab), index), cases, defs) =>
-    (thy, syntax, data, asms, binds,
+  (fn (syntax, asms, binds, (naming, (space, tab), index), cases, defs) =>
+    (syntax, asms, binds,
       (naming, (fold (NameSpace.hide fully) names space, tab), index), cases, defs));
 
 
@@ -1030,13 +956,13 @@
 
 fun put_thms ("", _) ctxt = ctxt
   | put_thms (bname, ths) ctxt = ctxt |> map_context
-      (fn (thy, syntax, data, asms, binds, (naming, (space, tab), index), cases, defs) =>
+      (fn (syntax, asms, binds, (naming, (space, tab), index), cases, defs) =>
         let
           val name = NameSpace.full naming bname;
           val space' = NameSpace.declare naming name space;
           val tab' = Symtab.update ((name, ths), tab);
           val index' = FactIndex.add (is_known ctxt) (name, ths) index;
-        in (thy, syntax, data, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
+        in (syntax, asms, binds, (naming, (space', tab'), index'), cases, defs) end);
 
 fun put_thm (name, th) = put_thms (name, [th]);
 val put_thmss = fold put_thms;
@@ -1044,10 +970,9 @@
 
 (* reset_thms *)
 
-fun reset_thms name =    (* FIXME hide!? *)
-  map_context (fn (thy, syntax, data, asms, binds, (q, (space, tab), index), cases, defs) =>
-    (thy, syntax, data, asms, binds, (q, (space, Symtab.delete_safe name tab), index),
-      cases, defs));
+fun reset_thms name =    (* FIXME NameSpace.hide!? *)
+  map_context (fn (syntax, asms, binds, (q, (space, tab), index), cases, defs) =>
+    (syntax, asms, binds, (q, (space, Symtab.delete_safe name tab), index), cases, defs));
 
 
 (* note_thmss *)
@@ -1150,8 +1075,8 @@
     val asmss = map #2 results;
     val thmss = map #3 results;
     val ctxt3 = ctxt2 |> map_context
-      (fn (thy, syntax, data, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
-        (thy, syntax, data, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
+      (fn (syntax, ((asms_ct, asms_th), fixes), binds, thms, cases, defs) =>
+        (syntax, ((asms_ct @ [(cprops, exp)], asms_th @ asmss), fixes), binds, thms,
           cases, defs));
     val ctxt4 = ctxt3 |> put_thms ("prems", prems_of ctxt3);
   in (warn_extra_tfrees ctxt ctxt4, thmss) end;
@@ -1198,8 +1123,8 @@
 local
 
 fun map_fixes f =
-  map_context (fn (thy, syntax, data, (assumes, fixes), binds, thms, cases, defs) =>
-    (thy, syntax, data, (assumes, f fixes), binds, thms, cases, defs));
+  map_context (fn (syntax, (assumes, fixes), binds, thms, cases, defs) =>
+    (syntax, (assumes, f fixes), binds, thms, cases, defs));
 
 fun err_dups ctxt xs = raise CONTEXT ("Duplicate variable(s): " ^ commas_quote xs, ctxt);
 
@@ -1303,13 +1228,13 @@
 
 in
 
-fun get_case (ctxt as Context {cases, ...}) name xs =
-  (case assoc (cases, name) of
+fun get_case ctxt name xs =
+  (case assoc_string (cases_of ctxt, name) of
     NONE => raise CONTEXT ("Unknown case: " ^ quote name, ctxt)
   | SOME c => prep_case ctxt name xs c);
 
-fun add_cases xs = map_context (fn (thy, syntax, data, asms, binds, thms, cases, defs) =>
-  (thy, syntax, data, asms, binds, thms, fold add_case xs cases, defs));
+fun add_cases xs = map_context (fn (syntax, asms, binds, thms, cases, defs) =>
+  (syntax, asms, binds, thms, fold add_case xs cases, defs));
 
 end;
 
@@ -1340,8 +1265,9 @@
 
 (* term bindings *)
 
-fun pretty_binds (ctxt as Context {binds, ...}) =
+fun pretty_binds ctxt =
   let
+    val binds = binds_of ctxt;
     fun prt_bind (xi, (t, T)) = pretty_term ctxt (Logic.mk_equals (Var (xi, T), t));
   in
     if Vartab.is_empty binds andalso not (! verbose) then []
@@ -1353,15 +1279,15 @@
 
 (* local theorems *)
 
-fun pretty_lthms (ctxt as Context {thms = (_, table, _), ...}) =
-  pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table table);
+fun pretty_lthms ctxt =
+  pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#2 (thms_of ctxt)));
 
 val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms;
 
 
 (* local contexts *)
 
-fun pretty_cases (ctxt as Context {cases, ...}) =
+fun pretty_cases ctxt =
   let
     val prt_term = pretty_term ctxt;
 
@@ -1383,6 +1309,8 @@
           (List.mapPartial (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
         (if forall (null o #2) asms then []
           else prt_sect "assume" [Pretty.str "and"] prt_asm asms)));
+
+    val cases = cases_of ctxt;
   in
     if null cases andalso not (! verbose) then []
     else [Pretty.big_list "cases:"
@@ -1429,7 +1357,7 @@
 
 (* main context *)
 
-fun pretty_context (ctxt as Context {cases, defs = (types, sorts, used, _), ...}) =
+fun pretty_context ctxt =
   let
     val prt_term = pretty_term ctxt;
     val prt_typ = pretty_typ ctxt;
@@ -1451,6 +1379,8 @@
 
     val prt_defT = prt_atom prt_var prt_typ;
     val prt_defS = prt_atom prt_varT prt_sort;
+
+    val (types, sorts, used, _) = defaults_of ctxt;
   in
     verb_single (K pretty_thy) @
     pretty_asms ctxt @