--- 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)
--- 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
--- 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;
--- 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) =
--- 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 =
--- 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 *)
--- 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
--- 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;
--- 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
--- 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 =
--- 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);
--- 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
--- 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;
--- 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,
--- 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*)
--- 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;
--- 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;
--- 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)
--- 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 _ =