# HG changeset patch # User wenzelm # Date 1302960325 -7200 # Node ID 6ca5407863ed1df277431154becaa6eab3ec1321 # Parent b47d41d9f4b5266dc6ec6d400a7ff99a3942db71 prefer local name spaces; tuned signatures; tuned; diff -r b47d41d9f4b5 -r 6ca5407863ed src/HOL/List.thy --- a/src/HOL/List.thy Sat Apr 16 13:48:45 2011 +0200 +++ b/src/HOL/List.thy Sat Apr 16 15:25:25 2011 +0200 @@ -396,7 +396,7 @@ fun abs_tr ctxt (p as Free (s, T)) e opti = let val thy = ProofContext.theory_of ctxt; - val s' = Sign.intern_const thy s; + val s' = ProofContext.intern_const ctxt s; in if Sign.declared_const thy s' then (pat_tr ctxt p e opti, false) diff -r b47d41d9f4b5 -r 6ca5407863ed src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Sat Apr 16 15:25:25 2011 +0200 @@ -307,7 +307,7 @@ fun case_tr err tab_of ctxt [t, u] = let val thy = ProofContext.theory_of ctxt; - val intern_const_syntax = Consts.intern_syntax (Sign.consts_of thy); + val intern_const_syntax = Consts.intern_syntax (ProofContext.consts_of ctxt); (* replace occurrences of dummy_pattern by distinct variables *) (* internalize constant names *) @@ -320,7 +320,7 @@ | prep_pat (Const (s, T)) used = (Const (intern_const_syntax s, T), used) | prep_pat (v as Free (s, T)) used = - let val s' = Sign.intern_const thy s in + let val s' = ProofContext.intern_const ctxt s in if Sign.declared_const thy s' then (Const (s', T), used) else (v, used) @@ -328,7 +328,7 @@ | prep_pat (t $ u) used = let val (t', used') = prep_pat t used; - val (u', used'') = prep_pat u used' + val (u', used'') = prep_pat u used'; in (t' $ u', used'') end diff -r b47d41d9f4b5 -r 6ca5407863ed src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Sat Apr 16 15:25:25 2011 +0200 @@ -378,12 +378,13 @@ fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy = let + val ctxt = ProofContext.init_global thy; + fun constr_of_term (Const (c, T)) = (c, T) - | constr_of_term t = - error ("Not a constant: " ^ Syntax.string_of_term_global thy t); - fun no_constr (c, T) = error ("Bad constructor: " - ^ Sign.extern_const thy c ^ "::" - ^ Syntax.string_of_typ_global thy T); + | constr_of_term t = error ("Not a constant: " ^ Syntax.string_of_term ctxt t); + fun no_constr (c, T) = + error ("Bad constructor: " ^ ProofContext.extern_const ctxt c ^ "::" ^ + Syntax.string_of_typ ctxt T); fun type_of_constr (cT as (_, T)) = let val frees = OldTerm.typ_tfrees T; @@ -437,8 +438,7 @@ #-> after_qed end; in - thy - |> ProofContext.init_global + ctxt |> Proof.theorem NONE after_qed' ((map o map) (rpair []) (flat rules)) end; diff -r b47d41d9f4b5 -r 6ca5407863ed src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/HOL/Tools/record.ML Sat Apr 16 15:25:25 2011 +0200 @@ -693,7 +693,7 @@ | split_args _ _ = ([], []); fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (Sign.intern_const thy name) of + (case get_fieldext thy (ProofContext.intern_const ctxt name) of SOME (ext, alphas) => (case get_extfields thy ext of SOME fields => @@ -753,7 +753,7 @@ | split_args _ _ = ([], []); fun mk_ext (fargs as (name, _) :: _) = - (case get_fieldext thy (Sign.intern_const thy name) of + (case get_fieldext thy (ProofContext.intern_const ctxt name) of SOME (ext, _) => (case get_extfields thy ext of SOME fields => @@ -831,7 +831,8 @@ (let val (f :: fs, _) = split_last fields; val fields' = - apfst (Sign.extern_const thy) f :: map (apfst Long_Name.base_name) fs; + apfst (ProofContext.extern_const ctxt) f :: + map (apfst Long_Name.base_name) fs; val (args', more) = split_last args; val alphavars = map varifyT (#1 (split_last alphas)); val subst = Type.raw_matches (alphavars, args') Vartab.empty; @@ -914,7 +915,6 @@ fun record_tr' ctxt t = let val thy = ProofContext.theory_of ctxt; - val extern = Consts.extern ctxt (ProofContext.consts_of ctxt); fun strip_fields t = (case strip_comb t of @@ -925,7 +925,7 @@ SOME fields => (let val (f :: fs, _) = split_last (map fst fields); - val fields' = extern f :: map Long_Name.base_name fs; + val fields' = ProofContext.extern_const ctxt f :: map Long_Name.base_name fs; val (args', more) = split_last args; in (fields' ~~ args') @ strip_fields more end handle ListPair.UnequalLengths => [("", t)]) @@ -957,7 +957,7 @@ fun dest_update ctxt c = (case try Lexicon.unmark_const c of - SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d) + SOME d => try (unsuffix updateN) (ProofContext.extern_const ctxt d) | NONE => NONE); fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/class.ML Sat Apr 16 15:25:25 2011 +0200 @@ -14,7 +14,7 @@ val these_defs: theory -> sort -> thm list val these_operations: theory -> sort -> (string * (class * (typ * term))) list - val print_classes: theory -> unit + val print_classes: Proof.context -> unit val init: class -> theory -> Proof.context val begin: class list -> sort -> Proof.context -> Proof.context val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory @@ -69,7 +69,7 @@ assm_intro: thm option, of_class: thm, axiom: thm option, - + (* dynamic part *) defs: thm list, operations: (string * (class * (typ * term))) list @@ -149,9 +149,9 @@ | NONE => base_morphism thy class; val export_morphism = #export_morph oo the_class_data; -fun print_classes thy = +fun print_classes ctxt = let - val ctxt = ProofContext.init_global thy; + val thy = ProofContext.theory_of ctxt; val algebra = Sign.classes_of thy; val arities = Symtab.empty @@ -163,10 +163,11 @@ let val Ss = Sorts.mg_domain algebra tyco [class]; in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end; - fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: " - ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty); + fun mk_param (c, ty) = + Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^ + Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty)); fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [ - (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"), + (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"), (SOME o Pretty.block) [Pretty.str "supersort: ", (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class], ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) @@ -500,18 +501,20 @@ val thy = ProofContext.theory_of lthy; fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort); fun pr_param ((c, _), (v, ty)) = - (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", - (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty]; + Pretty.block (Pretty.breaks + [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c), + Pretty.str "::", Syntax.pretty_typ lthy ty]); in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end; fun conclude lthy = let - val (tycos, vs, sort) = (#arities o the_instantiation) lthy; + val (tycos, vs, sort) = #arities (the_instantiation lthy); val thy = ProofContext.theory_of lthy; - val _ = map (fn tyco => if Sign.of_sort thy + val _ = tycos |> List.app (fn tyco => + if Sign.of_sort thy (Type (tyco, map TFree vs), sort) - then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco))) - tycos; + then () + else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco))); in lthy end; fun instantiation (tycos, vs, sort) thy = diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/code.ML Sat Apr 16 15:25:25 2011 +0200 @@ -112,9 +112,14 @@ fun string_of_typ thy = Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy)); -fun string_of_const thy c = case AxClass.inst_of_param thy c - of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) - | NONE => Sign.extern_const thy c; +fun string_of_const thy c = + let val ctxt = ProofContext.init_global thy in + case AxClass.inst_of_param thy c of + SOME (c, tyco) => + ProofContext.extern_const ctxt c ^ " " ^ enclose "[" "]" + (ProofContext.extern_type ctxt tyco) + | NONE => ProofContext.extern_const ctxt c + end; (* constants *) diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/expression.ML Sat Apr 16 15:25:25 2011 +0200 @@ -616,7 +616,7 @@ fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args => if length args = n then Syntax.const "_aprop" $ (* FIXME avoid old-style early externing (!??) *) - Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args) + Term.list_comb (Syntax.free (ProofContext.extern_const ctxt c), args) else raise Match); (* define one predicate including its intro rule and axioms diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Sat Apr 16 15:25:25 2011 +0200 @@ -162,7 +162,7 @@ val ctxt = ProofContext.init_global thy; in raw_rules |> map (Syntax.map_trrule (fn (r, s) => - Syntax_Phases.parse_ast_pattern ctxt (Sign.intern_type thy r, s))) + Syntax_Phases.parse_ast_pattern ctxt (ProofContext.intern_type ctxt r, s))) end; fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat Apr 16 15:25:25 2011 +0200 @@ -829,8 +829,8 @@ val _ = Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag - (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory - o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); + (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o + Toplevel.keep (Class.print_classes o Toplevel.context_of))); val _ = Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/overloading.ML Sat Apr 16 15:25:25 2011 +0200 @@ -158,11 +158,11 @@ fun pretty lthy = let - val thy = ProofContext.theory_of lthy; val overloading = get_overloading lthy; fun pr_operation ((c, ty), (v, _)) = - (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", - Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty]; + Pretty.block (Pretty.breaks + [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c), + Pretty.str "::", Syntax.pretty_typ lthy ty]); in Pretty.str "overloading" :: map pr_operation overloading end; fun conclude lthy = diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Apr 16 15:25:25 2011 +0200 @@ -37,6 +37,15 @@ val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context val facts_of: Proof.context -> Facts.T val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list + val class_space: Proof.context -> Name_Space.T + val type_space: Proof.context -> Name_Space.T + val const_space: Proof.context -> Name_Space.T + val intern_class: Proof.context -> xstring -> string + val intern_type: Proof.context -> xstring -> string + val intern_const: Proof.context -> xstring -> string + val extern_class: Proof.context -> string -> xstring + val extern_type: Proof.context -> string -> xstring + val extern_const: Proof.context -> string -> xstring val transfer_syntax: theory -> Proof.context -> Proof.context val transfer: theory -> Proof.context -> Proof.context val background_theory: (theory -> theory) -> Proof.context -> Proof.context @@ -269,6 +278,21 @@ val cases_of = #cases o rep_context; +(* name spaces *) + +val class_space = Type.class_space o tsig_of; +val type_space = Type.type_space o tsig_of; +val const_space = Consts.space_of o consts_of; + +val intern_class = Name_Space.intern o class_space; +val intern_type = Name_Space.intern o type_space; +val intern_const = Name_Space.intern o const_space; + +fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt); +fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt); +fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt); + + (* theory transfer *) fun transfer_syntax thy ctxt = ctxt |> @@ -351,7 +375,7 @@ in -val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort; +val read_arity = prep_arity intern_type Syntax.read_sort; val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of); end; @@ -452,7 +476,7 @@ TFree (c, default_sort ctxt (c, ~1))) else let - val d = Type.intern_type tsig c; + val d = intern_type ctxt c; val decl = Type.the_decl tsig d; val _ = Context_Position.report ctxt pos (Markup.tycon d); fun err () = error ("Bad type name: " ^ quote d); diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Sat Apr 16 15:25:25 2011 +0200 @@ -605,8 +605,6 @@ fun unparse_t t_to_ast prt_t markup ctxt t = let val syn = ProofContext.syn_of ctxt; - val tsig = ProofContext.tsig_of ctxt; - val consts = ProofContext.consts_of ctxt; fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x)) | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x)) @@ -622,9 +620,9 @@ SOME "" => ([], c) | SOME b => markup_extern b | NONE => c |> Lexicon.unmark - {case_class = fn x => ([Markup.tclass x], Type.extern_class ctxt tsig x), - case_type = fn x => ([Markup.tycon x], Type.extern_type ctxt tsig x), - case_const = fn x => ([Markup.const x], Consts.extern ctxt consts x), + {case_class = fn x => ([Markup.tclass x], ProofContext.extern_class ctxt x), + case_type = fn x => ([Markup.tycon x], ProofContext.extern_type ctxt x), + case_const = fn x => ([Markup.const x], ProofContext.extern_const ctxt x), case_fixed = fn x => free_or_skolem ctxt x, case_default = fn x => ([], x)}); in diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/Thy/thy_output.ML Sat Apr 16 15:25:25 2011 +0200 @@ -510,11 +510,11 @@ in ProofContext.pretty_term_abbrev ctxt' eq end; fun pretty_class ctxt = - Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt; + Pretty.str o ProofContext.extern_class ctxt o ProofContext.read_class ctxt; fun pretty_type ctxt s = let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s - in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end; + in Pretty.str (ProofContext.extern_type ctxt name) end; fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full; diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/display.ML --- a/src/Pure/display.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/display.ML Sat Apr 16 15:25:25 2011 +0200 @@ -195,7 +195,7 @@ val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes)); val tdecls = Name_Space.dest_table ctxt types; - val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities); + val arties = Name_Space.dest_table ctxt (Type.type_space tsig, arities); fun prune_const c = not verbose andalso Consts.is_concealed consts c; val cnsts = Name_Space.extern_table ctxt (#1 constants, diff -r b47d41d9f4b5 -r 6ca5407863ed src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Pure/sign.ML Sat Apr 16 15:25:25 2011 +0200 @@ -49,15 +49,12 @@ val class_space: theory -> Name_Space.T val type_space: theory -> Name_Space.T val const_space: theory -> Name_Space.T + val intern_class: theory -> xstring -> string + val intern_type: theory -> xstring -> string + val intern_const: theory -> xstring -> string val class_alias: binding -> class -> theory -> theory val type_alias: binding -> string -> theory -> theory val const_alias: binding -> string -> theory -> theory - val intern_class: theory -> xstring -> string - val extern_class: theory -> string -> xstring - val intern_type: theory -> xstring -> string - val extern_type: theory -> string -> xstring - val intern_const: theory -> xstring -> string - val extern_const: theory -> string -> xstring val arity_number: theory -> string -> int val arity_sorts: theory -> string -> sort -> sort list val certify_class: theory -> class -> class @@ -222,23 +219,20 @@ -(** intern / extern names **) +(** name spaces **) val class_space = Type.class_space o tsig_of; val type_space = Type.type_space o tsig_of; val const_space = Consts.space_of o consts_of; +val intern_class = Name_Space.intern o class_space; +val intern_type = Name_Space.intern o type_space; +val intern_const = Name_Space.intern o const_space; + fun class_alias b c thy = map_tsig (Type.class_alias (naming_of thy) b c) thy; fun type_alias b c thy = map_tsig (Type.type_alias (naming_of thy) b c) thy; fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy; -val intern_class = Name_Space.intern o class_space; -fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy); -val intern_type = Name_Space.intern o type_space; -fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy); -val intern_const = Name_Space.intern o const_space; -fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy); - (** certify entities **) (*exception TYPE*) diff -r b47d41d9f4b5 -r 6ca5407863ed src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Tools/Code/code_runtime.ML Sat Apr 16 15:25:25 2011 +0200 @@ -188,19 +188,23 @@ fun evaluation_code thy module_name tycos consts = let + val ctxt = ProofContext.init_global thy; val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts; val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos; - val (ml_code, target_names) = Code_Target.produce_code_for thy - target NONE module_name [] naming program (consts' @ tycos'); + val (ml_code, target_names) = + Code_Target.produce_code_for thy + target NONE module_name [] naming program (consts' @ tycos'); val (consts'', tycos'') = chop (length consts') target_names; - val consts_map = map2 (fn const => fn NONE => - error ("Constant " ^ (quote o Code.string_of_const thy) const - ^ "\nhas a user-defined serialization") - | SOME const'' => (const, const'')) consts consts'' - val tycos_map = map2 (fn tyco => fn NONE => - error ("Type " ^ (quote o Sign.extern_type thy) tyco - ^ "\nhas a user-defined serialization") - | SOME tyco'' => (tyco, tyco'')) tycos tycos''; + val consts_map = map2 (fn const => + fn NONE => + error ("Constant " ^ (quote o Code.string_of_const thy) const ^ + "\nhas a user-defined serialization") + | SOME const'' => (const, const'')) consts consts'' + val tycos_map = map2 (fn tyco => + fn NONE => + error ("Type " ^ quote (ProofContext.extern_type ctxt tyco) ^ + "\nhas a user-defined serialization") + | SOME tyco'' => (tyco, tyco'')) tycos tycos''; in (ml_code, (tycos_map, consts_map)) end; diff -r b47d41d9f4b5 -r 6ca5407863ed src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Tools/Code/code_target.ML Sat Apr 16 15:25:25 2011 +0200 @@ -307,13 +307,16 @@ fun project_program thy abortable names_hidden names1 program2 = let + val ctxt = ProofContext.init_global thy; val names2 = subtract (op =) names_hidden names1; val program3 = Graph.subgraph (not o member (op =) names_hidden) program2; val names4 = Graph.all_succs program3 names2; val empty_funs = filter_out (member (op =) abortable) (Code_Thingol.empty_funs program3); - val _ = if null empty_funs then () else error ("No code equations for " - ^ commas (map (Sign.extern_const thy) empty_funs)); + val _ = + if null empty_funs then () + else error ("No code equations for " ^ + commas (map (ProofContext.extern_const ctxt) empty_funs)); val program4 = Graph.subgraph (member (op =) names4) program3; in (names4, program4) end; diff -r b47d41d9f4b5 -r 6ca5407863ed src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/Tools/Code/code_thingol.ML Sat Apr 16 15:25:25 2011 +0200 @@ -489,20 +489,29 @@ end | _ => []; -fun labelled_name thy program name = case Graph.get_node program name - of Fun (c, _) => quote (Code.string_of_const thy c) - | Datatype (tyco, _) => "type " ^ quote (Sign.extern_type thy tyco) - | Datatypecons (c, _) => quote (Code.string_of_const thy c) - | Class (class, _) => "class " ^ quote (Sign.extern_class thy class) - | Classrel (sub, super) => let - val Class (sub, _) = Graph.get_node program sub - val Class (super, _) = Graph.get_node program super - in quote (Sign.extern_class thy sub ^ " < " ^ Sign.extern_class thy super) end - | Classparam (c, _) => quote (Code.string_of_const thy c) - | Classinst ((class, (tyco, _)), _) => let - val Class (class, _) = Graph.get_node program class - val Datatype (tyco, _) = Graph.get_node program tyco - in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end +fun labelled_name thy program name = + let val ctxt = ProofContext.init_global thy in + case Graph.get_node program name of + Fun (c, _) => quote (Code.string_of_const thy c) + | Datatype (tyco, _) => "type " ^ quote (ProofContext.extern_type ctxt tyco) + | Datatypecons (c, _) => quote (Code.string_of_const thy c) + | Class (class, _) => "class " ^ quote (ProofContext.extern_class ctxt class) + | Classrel (sub, super) => + let + val Class (sub, _) = Graph.get_node program sub; + val Class (super, _) = Graph.get_node program super; + in + quote (ProofContext.extern_class ctxt sub ^ " < " ^ ProofContext.extern_class ctxt super) + end + | Classparam (c, _) => quote (Code.string_of_const thy c) + | Classinst ((class, (tyco, _)), _) => + let + val Class (class, _) = Graph.get_node program class; + val Datatype (tyco, _) = Graph.get_node program tyco; + in + quote (ProofContext.extern_type ctxt tyco ^ " :: " ^ ProofContext.extern_class ctxt class) + end + end; fun linear_stmts program = rev (Graph.strong_conn program) diff -r b47d41d9f4b5 -r 6ca5407863ed src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Sat Apr 16 13:48:45 2011 +0200 +++ b/src/ZF/Tools/inductive_package.ML Sat Apr 16 15:25:25 2011 +0200 @@ -143,7 +143,7 @@ If no mutual recursion then it equals the one recursive set. If mutual recursion then it differs from all the recursive sets. *) val big_rec_base_name = space_implode "_" rec_base_names; - val big_rec_name = Sign.intern_const thy big_rec_base_name; + val big_rec_name = ProofContext.intern_const ctxt big_rec_base_name; val _ =