--- a/src/HOL/Tools/datatype_package.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Sat Jun 11 22:15:48 2005 +0200
@@ -99,7 +99,7 @@
fun print sg tab =
Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (Sign.extern_table sg Sign.typeK tab)));
+ map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
end;
structure DatatypesData = TheoryDataFun(DatatypesArgs);
@@ -466,7 +466,7 @@
(loose_bnos (strip_abs_body t))
end;
val cases = map (fn ((cname, dts), t) =>
- (Sign.extern sg Sign.constK cname,
+ (Sign.extern_const sg cname,
strip_abs (length dts) t, is_dependent (length dts) t))
(constrs ~~ fs);
fun count_cases (cs, (_, _, true)) = cs
--- a/src/HOL/Tools/inductive_package.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sat Jun 11 22:15:48 2005 +0200
@@ -101,7 +101,8 @@
(Symtab.merge (K true) (tab1, tab2), Drule.merge_rules (monos1, monos2));
fun print sg (tab, monos) =
- [Pretty.strs ("(co)inductives:" :: map #1 (Sign.extern_table sg Sign.constK tab)),
+ [Pretty.strs ("(co)inductives:" ::
+ map #1 (NameSpace.extern_table (Sign.const_space sg, tab))),
Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
|> Pretty.chunks |> Pretty.writeln;
end;
--- a/src/HOL/Tools/recdef_package.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sat Jun 11 22:15:48 2005 +0200
@@ -120,8 +120,8 @@
Drule.merge_rules (wfs1, wfs2)));
fun print sg (tab, hints) =
- (Pretty.strs ("recdefs:" :: map #1 (Sign.extern_table sg Sign.constK tab)) ::
- pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
+ (Pretty.strs ("recdefs:" :: map #1 (NameSpace.extern_table (Sign.const_space sg, tab))) ::
+ pretty_hints hints) |> Pretty.chunks |> Pretty.writeln;
end;
structure GlobalRecdefData = TheoryDataFun(GlobalRecdefArgs);
--- a/src/HOL/Tools/record_package.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Jun 11 22:15:48 2005 +0200
@@ -287,7 +287,7 @@
[Pretty.block [prt_typ (Type (name, Ts)), Pretty.str " +"]];
fun pretty_field (c, T) = Pretty.block
- [Pretty.str (Sign.extern sg Sign.constK c), Pretty.str " ::",
+ [Pretty.str (Sign.extern_const sg c), Pretty.str " ::",
Pretty.brk 1, Pretty.quote (prt_typ T)];
fun pretty_record (name, {args, parent, fields, ...}: record_info) =
@@ -670,7 +670,7 @@
SOME flds
=> (let
val (f::fs) = but_last (map fst flds);
- val flds' = Sign.extern sg Sign.constK f::map NameSpace.base fs;
+ val flds' = Sign.extern_const sg f :: map NameSpace.base fs;
val (args',more) = split_last args;
in (flds'~~args')@field_lst more end
handle UnequalLengths => [("",t)])
@@ -775,7 +775,7 @@
SOME (_,alphas)
=> (let
val (f::fs) = but_last flds;
- val flds' = apfst (Sign.extern sg Sign.constK) f
+ val flds' = apfst (Sign.extern_const sg) f
::map (apfst NameSpace.base) fs;
val (args',more) = split_last args;
val alphavars = map Type.varifyT (but_last alphas);
--- a/src/HOLCF/holcf_logic.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/HOLCF/holcf_logic.ML Sat Jun 11 22:15:48 2005 +0200
@@ -47,7 +47,7 @@
(*cfun, ssum, sprod, u, tr, one *)
-local val intern = Sign.intern_tycon HOLCF_sg;
+local val intern = Sign.intern_type HOLCF_sg;
in
val cfun_arrow = intern "->";
val op ->> = mk_btyp cfun_arrow;
--- a/src/Pure/axclass.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/Pure/axclass.ML Sat Jun 11 22:15:48 2005 +0200
@@ -131,12 +131,9 @@
fun print sg tab =
let
- val ext_class = Sign.extern sg Sign.classK;
- val ext_thm = PureThy.extern_thm_sg sg;
-
fun pretty_class c cs = Pretty.block
- (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
- Pretty.breaks (map (Pretty.str o ext_class) cs));
+ (Pretty.str (Sign.extern_class sg c) :: Pretty.str " <" :: Pretty.brk 1 ::
+ Pretty.breaks (map (Pretty.str o Sign.extern_class sg) cs));
fun pretty_thms name thms = Pretty.big_list (name ^ ":")
(map (Display.pretty_thm_sg sg) thms);
@@ -282,7 +279,7 @@
fun prep_arity prep_tycon prep_sort prep sg (t, Ss, x) =
test_arity sg (prep_tycon sg t, map (prep_sort sg) Ss, prep sg x);
-val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
+val read_arity = prep_arity Sign.intern_type Sign.read_sort Sign.read_sort;
val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
--- a/src/Pure/codegen.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/Pure/codegen.ML Sat Jun 11 22:15:48 2005 +0200
@@ -300,7 +300,7 @@
let
val {codegens, tycodegens, consts, types, attrs, preprocs, test_params} =
CodegenData.get thy;
- val tc = Sign.intern_tycon (sign_of thy) s
+ val tc = Sign.intern_type (sign_of thy) s
in
(case assoc (types, tc) of
NONE => CodegenData.put {codegens = codegens,
@@ -342,11 +342,11 @@
end;
fun mk_const_id sg s =
- let val s' = mk_id (Sign.extern sg Sign.constK s)
+ let val s' = mk_id (Sign.extern_const sg s)
in if s' mem ThmDatabase.ml_reserved then s' ^ "_const" else s' end;
fun mk_type_id sg s =
- let val s' = mk_id (Sign.extern sg Sign.typeK s)
+ let val s' = mk_id (Sign.extern_type sg s)
in if s' mem ThmDatabase.ml_reserved then s' ^ "_type" else s' end;
fun rename_terms ts =
--- a/src/Pure/display.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/Pure/display.ML Sat Jun 11 22:15:48 2005 +0200
@@ -199,14 +199,14 @@
prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S];
val tfrees = map (fn v => TFree (v, []));
- fun pretty_type syn (t, Type.LogicalType n) =
+ fun pretty_type syn (t, (Type.LogicalType n, _)) =
if syn then NONE
else SOME (prt_typ (Type (t, tfrees (Term.invent_names [] "'a" n))))
- | pretty_type syn (t, Type.Abbreviation (vs, U, syn')) =
+ | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) =
if syn <> syn' then NONE
else SOME (Pretty.block
[prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U])
- | pretty_type syn (t, Type.Nonterminal) =
+ | pretty_type syn (t, (Type.Nonterminal, _)) =
if not syn then NONE
else SOME (prt_typ (Type (t, [])));
@@ -224,20 +224,20 @@
val {sign = _, defs, axioms, oracles, parents = _, ancestors = _} = Theory.rep_theory thy;
- val {self = _, tsig, consts, naming, spaces = _, data} = Sign.rep_sg sg;
+ val {self = _, tsig, consts, naming, data} = Sign.rep_sg sg;
val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
- val tdecls = Symtab.dest types |> map (fn (t, (d, _)) =>
- (Sign.extern sg Sign.typeK t, (t, d))) |> Library.sort_wrt #1 |> map #2;
- val cnsts = Sign.extern_table sg Sign.constK consts;
- val finals = Sign.extern_table sg Sign.constK (Defs.finals defs);
+ val clsses = NameSpace.extern_table (apsnd (Symtab.make o Graph.dest) classes);
+ val tdecls = NameSpace.extern_table types;
+ val cnsts = NameSpace.extern_table consts;
+ val finals = NameSpace.extern_table (#1 consts, Defs.finals defs);
val axms = NameSpace.extern_table axioms;
val oras = NameSpace.extern_table oracles;
in
[Pretty.strs ("stamps:" :: Sign.stamp_names_of sg),
Pretty.strs ("data:" :: Sign.data_kinds data),
Pretty.strs ["name prefix:", NameSpace.path_of naming],
- Pretty.big_list "classes:" (map pretty_classrel (Graph.dest classes)),
+ Pretty.big_list "classes:" (map pretty_classrel clsses),
pretty_default default,
pretty_witness witness,
Pretty.big_list "syntactic types:" (List.mapPartial (pretty_type true) tdecls),
--- a/src/ZF/Tools/induct_tacs.ML Sat Jun 11 22:15:47 2005 +0200
+++ b/src/ZF/Tools/induct_tacs.ML Sat Jun 11 22:15:48 2005 +0200
@@ -42,7 +42,7 @@
fun print sg tab =
Pretty.writeln (Pretty.strs ("datatypes:" ::
- map #1 (Sign.extern_table sg Sign.typeK tab)));
+ map #1 (NameSpace.extern_table (Sign.type_space sg, tab))));
end;
structure DatatypesData = TheoryDataFun(DatatypesArgs);