# HG changeset patch # User wenzelm # Date 1139534568 -3600 # Node ID 64e4b5bc644302b36894c7f1d812ea8638680e28 # Parent 1f73a35743f46aeb0c64db4c2cde70256cbbbf7e tuned comment; moved local syntax to local_syntax.ML; common naming (for abbrevs and thms); transfer: merge consts; tuned pretty_term'; added polymorphic -- special case of generalize; added add_abbrevs(_i); read/cert: expand_consts; diff -r 1f73a35743f4 -r 64e4b5bc6443 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Feb 10 02:22:46 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Feb 10 02:22:48 2006 +0100 @@ -2,11 +2,11 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -The key concept of Isar proof contexts. +The key concept of Isar proof contexts: elevates primitive local +reasoning Gamma |- phi to a structured concept, with generic context +elements, polymorphic abbreviations, and extra-logical data. *) -val show_structs = ref false; - signature PROOF_CONTEXT = sig type context (*= Context.proof*) @@ -69,6 +69,7 @@ val read_const: context -> string -> term val warn_extra_tfrees: context -> context -> context val generalize: context -> context -> term list -> term list + val polymorphic: context -> term list -> term list val export_standard: context -> context -> thm -> thm val exports: context -> context -> thm -> thm Seq.seq val goal_exports: context -> context -> thm -> thm Seq.seq @@ -144,6 +145,8 @@ val add_cases: bool -> (string * RuleCases.T option) list -> context -> context val apply_case: RuleCases.T -> context -> (string * term list) list * context val get_case: context -> string -> string option list -> RuleCases.T + val add_abbrevs: bool -> (bstring * string * mixfix) list -> context -> context + val add_abbrevs_i: bool -> (bstring * term * mixfix) list -> context -> context val verbose: bool ref val setmp_verbose: ('a -> 'b) -> 'a -> 'b val print_syntax: context -> unit @@ -163,6 +166,8 @@ type context = Context.proof; val theory_of = Context.theory_of_proof; +val tsig_of = Sign.tsig_of o theory_of; + val init = Context.init_proof; @@ -173,36 +178,33 @@ datatype ctxt = Ctxt of - {syntax: (*global/local syntax, structs, mixfixed*) - (Syntax.syntax * Syntax.syntax * (Syntax.syntax -> Syntax.syntax)) * - string list * string list, - consts: Consts.T, (*const abbreviations*) - fixes: bool * (string * string) list, (*fixes: !!x. _ with proof body flag*) + {naming: NameSpace.naming, (*local naming conventions*) + syntax: LocalSyntax.T, (*local syntax*) + consts: Consts.T, (*const abbreviations*) + fixes: bool * (string * string) list, (*fixes: !!x. _ with proof body flag*) assms: - ((cterm list * export) list * (*assumes and views: A ==> _*) - (string * thm list) list), (*prems: A |- A*) - binds: (typ * term) Vartab.table, (*term bindings*) - thms: NameSpace.naming * (*local thms*) - thm list NameSpace.table * FactIndex.T, - cases: (string * (RuleCases.T * bool)) list, (*local contexts*) + ((cterm list * export) list * (*assumes and views: A ==> _*) + (string * thm list) list), (*prems: A |- A*) + binds: (typ * term) Vartab.table, (*term bindings*) + thms: thm list NameSpace.table * FactIndex.T, (*local thms*) + cases: (string * (RuleCases.T * bool)) list, (*local contexts*) defaults: - typ Vartab.table * (*type constraints*) - sort Vartab.table * (*default sorts*) - string list * (*used type variables*) - term list Symtab.table}; (*type variable occurrences*) + 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, consts, fixes, assms, binds, thms, cases, defaults) = - Ctxt {syntax = syntax, consts = consts, fixes = fixes, assms = assms, binds = binds, - thms = thms, cases = cases, defaults = defaults}; +fun make_ctxt (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) = + Ctxt {naming = naming, syntax = syntax, consts = consts, fixes = fixes, assms = assms, + binds = binds, thms = thms, cases = cases, defaults = defaults}; structure ContextData = ProofDataFun ( val name = "Isar/context"; type T = ctxt; fun init thy = - make_ctxt (((Sign.syn_of thy, Sign.syn_of thy, I), [], []), Sign.consts_of thy, - (false, []), ([], []), Vartab.empty, - (NameSpace.default_naming, NameSpace.empty_table, FactIndex.empty), [], + make_ctxt (NameSpace.default_naming, LocalSyntax.init thy, Sign.consts_of thy, + (false, []), ([], []), Vartab.empty, (NameSpace.empty_table, FactIndex.empty), [], (Vartab.empty, Vartab.empty, [], Symtab.empty)); fun print _ _ = (); ); @@ -212,36 +214,50 @@ fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args); fun map_context f = - ContextData.map (fn Ctxt {syntax, consts, fixes, assms, binds, thms, cases, defaults} => - make_ctxt (f (syntax, consts, fixes, assms, binds, thms, cases, defaults))); + ContextData.map (fn Ctxt {naming, syntax, consts, fixes, assms, binds, thms, cases, defaults} => + make_ctxt (f (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults))); -fun map_syntax f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (f syntax, consts, fixes, assms, binds, thms, cases, defaults)); +fun map_naming f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (f naming, syntax, consts, fixes, assms, binds, thms, cases, defaults)); -fun map_consts f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, f consts, fixes, assms, binds, thms, cases, defaults)); +fun map_syntax f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, f syntax, consts, fixes, assms, binds, thms, cases, defaults)); -fun map_fixes f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, f fixes, assms, binds, thms, cases, defaults)); +fun map_consts f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, f consts, fixes, assms, binds, thms, cases, defaults)); + +fun map_fixes f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, f fixes, assms, binds, thms, cases, defaults)); -fun map_assms f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, fixes, f assms, binds, thms, cases, defaults)); +fun map_assms f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, fixes, f assms, binds, thms, cases, defaults)); -fun map_binds f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, fixes, assms, f binds, thms, cases, defaults)); +fun map_binds f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, fixes, assms, f binds, thms, cases, defaults)); -fun map_thms f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, fixes, assms, binds, f thms, cases, defaults)); - -fun map_naming f = map_thms (fn (naming, table, index) => (f naming, table, index)); +fun map_thms f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, fixes, assms, binds, f thms, cases, defaults)); -fun map_cases f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, fixes, assms, binds, thms, f cases, defaults)); +fun map_cases f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, fixes, assms, binds, thms, f cases, defaults)); -fun map_defaults f = map_context (fn (syntax, consts, fixes, assms, binds, thms, cases, defaults) => - (syntax, consts, fixes, assms, binds, thms, cases, f defaults)); +fun map_defaults f = + map_context (fn (naming, syntax, consts, fixes, assms, binds, thms, cases, defaults) => + (naming, syntax, consts, fixes, assms, binds, thms, cases, f defaults)); + +val naming_of = #naming o rep_context; val syntax_of = #syntax o rep_context; +val syn_of = LocalSyntax.syn_of o syntax_of; + val consts_of = #consts o rep_context; val is_body = #1 o #fixes o rep_context; @@ -258,7 +274,7 @@ val binds_of = #binds o rep_context; val thms_of = #thms o rep_context; -val fact_index_of = #3 o thms_of; +val fact_index_of = #2 o thms_of; val cases_of = #cases o rep_context; @@ -269,105 +285,29 @@ fun is_known ctxt x = Vartab.defined (#1 (defaults_of ctxt)) (x, ~1) orelse is_fixed ctxt x; - -(** syntax **) - -(* translation functions *) - -fun context_tr' ctxt = - let - val (_, structs, mixfixed) = syntax_of ctxt; - - fun tr' (t $ u) = tr' t $ tr' u - | tr' (Abs (x, T, t)) = Abs (x, T, tr' t) - | tr' (t as Free (x, T)) = - let val i = Library.find_index_eq x structs + 1 in - if i = 0 andalso member (op =) mixfixed x then Const (Syntax.fixedN ^ x, T) - else if i = 1 andalso not (! show_structs) then - Syntax.const "_struct" $ Syntax.const "_indexdefault" - else t - end - | tr' a = a; - in tr' end; - - -(* add syntax *) - -local - -fun check_mixfix (x, _, mx) = - if mx <> NoSyn andalso mx <> Structure andalso - (can Syntax.dest_internal x orelse can Syntax.dest_skolem x) then - error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) - else (); - -fun mixfix x NONE mx = (Syntax.fixedN ^ x, TypeInfer.mixfixT mx, Syntax.fix_mixfix x mx) - | mixfix x (SOME T) mx = (Syntax.fixedN ^ x, T, Syntax.fix_mixfix x mx); - -fun prep_mixfix (_, _, Structure) = NONE - | prep_mixfix (x, opt_T, mx) = SOME (mixfix x opt_T mx); - -fun prep_mixfix' (_, _, Structure) = NONE - | prep_mixfix' (x, _, NoSyn) = NONE - | prep_mixfix' (x, opt_T, _) = SOME (x, mixfix x opt_T (Syntax.literal x)); +(* transfer *) -fun prep_struct (x, _, Structure) = SOME x - | prep_struct _ = NONE; - -fun mk trs = map Syntax.mk_trfun trs; - -fun extend_syntax thy extend (global_syn, syn, mk_syn) = - let - val thy_syn = Sign.syn_of thy; - val mk_syn' = extend o mk_syn; - val (global_syn', syn') = - if Syntax.eq_syntax (global_syn, thy_syn) - then (global_syn, extend syn) - else (thy_syn, mk_syn' thy_syn); (*potentially expensive*) - in (global_syn', syn', mk_syn') end; - -in - -fun add_syntax decls ctxt = ctxt |> map_syntax (fn syntax => - let - val (syns, structs, mixfixed) = syntax; - val thy = theory_of ctxt; +fun transfer_syntax thy = + map_syntax (LocalSyntax.rebuild thy) #> + map_consts (fn consts => Consts.merge (Sign.consts_of thy, consts)); - val is_logtype = Sign.is_logtype thy; - val structs' = structs @ List.mapPartial prep_struct decls; - val mxs = List.mapPartial (tap check_mixfix #> prep_mixfix) decls; - val (fixed, mxs_output) = Library.split_list (List.mapPartial prep_mixfix' decls); - - val extend = - Syntax.extend_const_gram is_logtype ("", false) mxs_output - #> Syntax.extend_const_gram is_logtype ("", true) mxs; - val syns' = extend_syntax thy extend syns; - in (syns', structs', fixed @ mixfixed) end); - -fun syn_of' thy ctxt = - let - val (syns, structs, _) = syntax_of ctxt; - val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs; - val extend = Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs'); - in #2 (extend_syntax thy extend syns) end; - -fun syn_of ctxt = syn_of' (theory_of ctxt) ctxt; - -end; - -fun transfer thy = add_syntax [] o Context.transfer_proof thy; +fun transfer thy = Context.transfer_proof thy #> transfer_syntax thy; (** pretty printing **) -fun pretty_term' thy ctxt t = +fun pretty_term' abbrevs ctxt t = let + val thy = theory_of ctxt; + val syntax = syntax_of ctxt; val consts = consts_of ctxt; - val t' = Pattern.rewrite_term thy (Consts.abbrevs_of consts) [] t; - in Sign.pretty_term' (syn_of' thy ctxt) consts (Context.Proof ctxt) (context_tr' ctxt t) end; + val t' = t + |> K abbrevs ? Pattern.rewrite_term thy (Consts.abbrevs_of consts) [] + |> LocalSyntax.extern_term (NameSpace.extern (Consts.space_of consts)) thy syntax; + in Sign.pretty_term' (LocalSyntax.syn_of syntax) (Context.Proof ctxt) t' end; -fun pretty_term ctxt t = pretty_term' (theory_of ctxt) ctxt (context_tr' ctxt t); +val pretty_term = pretty_term' true; fun pretty_typ ctxt T = Sign.pretty_typ (theory_of ctxt) T; fun pretty_sort ctxt S = Sign.pretty_sort (theory_of ctxt) S; fun pretty_classrel ctxt cs = Sign.pretty_classrel (theory_of ctxt) cs; @@ -389,7 +329,7 @@ Pretty.block (Pretty.fbreaks (Pretty.str (a ^ ":") :: map (pretty_thm ctxt) ths)); fun pretty_proof ctxt prf = - pretty_term' (ProofSyntax.proof_syntax prf (theory_of ctxt)) ctxt + pretty_term' true (ctxt |> transfer_syntax (ProofSyntax.proof_syntax prf (theory_of ctxt))) (ProofSyntax.term_of_proof prf); fun pretty_proof_of ctxt full th = @@ -524,20 +464,22 @@ #1 o read_def_termTs freeze pp syn thy defaults o map (rpair propT); -(* norm_term *) +(* local abbreviations *) -fun norm_term ctxt schematic = +fun expand_consts ctxt = + Consts.certify (pp ctxt) (tsig_of ctxt) (consts_of ctxt); + +fun expand_binds ctxt schematic = let val binds = binds_of ctxt; - val tsig = Sign.tsig_of (theory_of ctxt); - fun norm_var (xi, T) = + fun expand_var (xi, T) = (case Vartab.lookup binds xi of - SOME t => Envir.expand_atom tsig T t + SOME t => Envir.expand_atom (tsig_of ctxt) T t | NONE => if schematic then Var (xi, T) else error ("Unbound schematic variable: " ^ Syntax.string_of_vname xi)); - in Envir.beta_norm o Term.map_aterms (fn Var v => norm_var v | a => a) end; + in Envir.beta_norm o Term.map_aterms (fn Var v => expand_var v | a => a) end; (* dummy patterns *) @@ -569,7 +511,8 @@ (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) s handle TERM (msg, _) => error msg) |> app (intern_skolem ctxt internal) - |> app (if pattern then I else norm_term ctxt schematic) + |> app (expand_consts ctxt) + |> app (if pattern then I else expand_binds ctxt schematic) |> app (if pattern then prepare_dummies else reject_dummies) end; @@ -602,7 +545,8 @@ local fun gen_cert prop pattern schematic ctxt t = t - |> (if pattern then I else norm_term ctxt schematic) + |> expand_consts ctxt + |> (if pattern then I else expand_binds ctxt schematic) |> (fn t' => #1 (Sign.certify false prop (pp ctxt) (theory_of ctxt) t') handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg); @@ -651,8 +595,9 @@ #> map_defaults (fn (types, sorts, used, occ) => (types, ins_sorts t sorts, used, occ)) #> map_defaults (fn (types, sorts, used, occ) => (types, sorts, ins_used t used, occ)); -fun declare_var (x, opt_T, mx) = - declare_syntax (Free (x, case opt_T of SOME T => T | NONE => TypeInfer.mixfixT mx)); +fun declare_var (x, opt_T, mx) ctxt = + let val T = (case opt_T of SOME T => T | NONE => TypeInfer.mixfixT mx) + in ((x, T, mx), ctxt |> declare_syntax (Free (x, T))) end; fun declare_term t ctxt = ctxt @@ -745,6 +690,18 @@ in map (Term.map_term_types (Term.map_type_tfree gen)) ts end; +(* polymorphic terms *) + +fun polymorphic ctxt ts = + generalize (ctxt |> fold declare_term ts) ctxt ts; + +fun extra_tvars t = + let val tvarsT = Term.add_tvarsT (Term.fastype_of t) [] in + Term.fold_types (Term.fold_atyps + (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [] + end; + + (** export theorems **) @@ -796,7 +753,7 @@ let val T = Term.fastype_of t; val t' = - if null (Term.term_tvars t \\ Term.typ_tvars T) then t + if null (extra_tvars t) then t else Var ((x ^ "_has_extra_type_vars_on_rhs", i), T); in declare_term t' #> map_binds (Vartab.update ((x, i), (T, t'))) end; @@ -950,7 +907,7 @@ fun some_fact_tac ctxt = SUBGOAL (fn (goal, i) => let - val (_, _, index) = thms_of ctxt; + val index = fact_index_of ctxt; val facts = FactIndex.could_unify index (Term.strip_all_body goal); in fact_tac facts i end); @@ -966,7 +923,7 @@ | retrieve_thms from_thy pick ctxt xthmref = let val thy = theory_of ctxt; - val (_, (space, tab), _) = thms_of ctxt; + val (space, tab) = #1 (thms_of ctxt); val thmref = PureThy.map_name_of_thmref (NameSpace.intern space) xthmref; val name = PureThy.name_of_thmref thmref; in @@ -999,36 +956,36 @@ (* name space operations *) -val extern_thm = NameSpace.extern o #1 o #2 o thms_of; +val extern_thm = NameSpace.extern o #1 o #1 o thms_of; 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; -val restore_naming = map_naming o K o #1 o thms_of; +val restore_naming = map_naming o K o naming_of; -fun hide_thms fully names = map_thms (fn (naming, (space, tab), index) => - (naming, (fold (NameSpace.hide fully) names space, tab), index)); +fun hide_thms fully names = map_thms (fn ((space, tab), index) => + ((fold (NameSpace.hide fully) names space, tab), index)); (* put_thms *) fun put_thms ("", NONE) ctxt = ctxt - | put_thms ("", SOME ths) ctxt = ctxt |> map_thms (fn (naming, facts, index) => + | put_thms ("", SOME ths) ctxt = ctxt |> map_thms (fn (facts, index) => let val index' = FactIndex.add_local (is_known ctxt) ("", ths) index; - in (naming, facts, index') end) - | put_thms (bname, NONE) ctxt = ctxt |> map_thms (fn (naming, (space, tab), index) => + in (facts, index') end) + | put_thms (bname, NONE) ctxt = ctxt |> map_thms (fn ((space, tab), index) => let - val name = NameSpace.full naming bname; + val name = NameSpace.full (naming_of ctxt) bname; val tab' = Symtab.delete_safe name tab; - in (naming, (space, tab'), index) end) - | put_thms (bname, SOME ths) ctxt = ctxt |> map_thms (fn (naming, (space, tab), index) => + in ((space, tab'), index) end) + | put_thms (bname, SOME ths) ctxt = ctxt |> map_thms (fn ((space, tab), index) => let - val name = NameSpace.full naming bname; - val space' = NameSpace.declare naming name space; + val name = NameSpace.full (naming_of ctxt) bname; + val space' = NameSpace.declare (naming_of ctxt) name space; val tab' = Symtab.update (name, ths) tab; val index' = FactIndex.add_local (is_known ctxt) (name, ths) index; - in (naming, (space', tab'), index') end); + in ((space', tab'), index') end); (* note_thmss *) @@ -1077,7 +1034,7 @@ else Type.no_tvars T handle TYPE (msg, _, _) => error msg; val opt_T = Option.map (cond_tvars o prep_typ ctxt) raw_T; val var = (x, opt_T, mx); - in (var, ctxt |> declare_var var) end); + in (var, ctxt |> declare_var var |> #2) end); in @@ -1089,10 +1046,45 @@ end; +(* abbreviations *) + +local + +fun gen_abbrevs prep_vars prep_term revert = fold (fn (raw_c, raw_t, raw_mx) => fn ctxt => + let + val ([(c, _, mx)], _) = prep_vars [(raw_c, NONE, raw_mx)] ctxt; + val [t] = polymorphic ctxt [prep_term ctxt raw_t]; + val _ = + if null (extra_tvars t) then () + else error ("Extra type variables on rhs of abbreviation: " ^ quote c); + in + ctxt + |> declare_term t + |> map_consts (Consts.abbreviate (pp ctxt) (tsig_of ctxt) (naming_of ctxt) revert (c, t)) + end); + +in + +val add_abbrevs = gen_abbrevs read_vars read_term; +val add_abbrevs_i = gen_abbrevs cert_vars cert_term; + +end; + + (* fixes *) local +fun prep_mixfix (x, T, mx) = + if mx <> Structure andalso (can Syntax.dest_internal x orelse can Syntax.dest_skolem x) then + error ("Illegal mixfix syntax for internal/skolem constant " ^ quote x) + else (true, (x, T, mx)); + +fun add_syntax raw_decls ctxt = + (case filter_out (equal NoSyn o #3) raw_decls of + [] => ctxt + | decls => ctxt |> map_syntax (LocalSyntax.add_syntax (theory_of ctxt) (map prep_mixfix decls))); + fun no_dups _ [] = () | no_dups ctxt dups = error ("Duplicate fixed variable(s): " ^ commas_quote dups); @@ -1105,12 +1097,11 @@ val xs' = if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs) else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs); - val vars' = map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars; in ctxt' |> map_fixes (fn (b, fixes) => (b, rev (xs ~~ xs') @ fixes)) - |> add_syntax vars' - |> fold declare_var vars' + |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars) + |-> add_syntax |> pair xs' end; @@ -1330,7 +1321,7 @@ val abbrevs = NameSpace.extern_table (space, Symtab.make (Symtab.fold local_abbrev consts [])); in if null abbrevs andalso not (! verbose) then [] - else [Pretty.big_list "abbreviations:" (map (pretty_term ctxt o #2) abbrevs)] + else [Pretty.big_list "abbreviations:" (map (pretty_term' false ctxt o #2) abbrevs)] end; @@ -1339,7 +1330,7 @@ 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)); + fun prt_bind (xi, (T, t)) = pretty_term' false ctxt (Logic.mk_equals (Var (xi, T), t)); in if Vartab.is_empty binds andalso not (! verbose) then [] else [Pretty.big_list "term bindings:" (map prt_bind (Vartab.dest binds))] @@ -1351,7 +1342,7 @@ (* local theorems *) fun pretty_lthms ctxt = - pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#2 (thms_of ctxt))); + pretty_items (pretty_thm ctxt) "facts:" (NameSpace.extern_table (#1 (thms_of ctxt))); val print_lthms = Pretty.writeln o Pretty.chunks o pretty_lthms; @@ -1403,7 +1394,7 @@ val prt_term = pretty_term ctxt; (*structures*) - val (_, structs, _) = syntax_of ctxt; + val structs = LocalSyntax.structs_of (syntax_of ctxt); val prt_structs = if null structs then [] else [Pretty.block (Pretty.str "structures:" :: Pretty.brk 1 :: Pretty.commas (map Pretty.str structs))];