# HG changeset patch # User wenzelm # Date 1118520948 -7200 # Node ID dc9f7066d80a76e7e68405e2904a3c8331650a8b # Parent c686a606dfbaa822ba1da06d3baa053d26a98fc2 refer to name spaces values instead of names; diff -r c686a606dfba -r dc9f7066d80a src/HOL/Tools/datatype_package.ML --- 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 diff -r c686a606dfba -r dc9f7066d80a src/HOL/Tools/inductive_package.ML --- 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; diff -r c686a606dfba -r dc9f7066d80a src/HOL/Tools/recdef_package.ML --- 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); diff -r c686a606dfba -r dc9f7066d80a src/HOL/Tools/record_package.ML --- 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); diff -r c686a606dfba -r dc9f7066d80a src/HOLCF/holcf_logic.ML --- 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; diff -r c686a606dfba -r dc9f7066d80a src/Pure/axclass.ML --- 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; diff -r c686a606dfba -r dc9f7066d80a src/Pure/codegen.ML --- 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 = diff -r c686a606dfba -r dc9f7066d80a src/Pure/display.ML --- 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), diff -r c686a606dfba -r dc9f7066d80a src/ZF/Tools/induct_tacs.ML --- 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);