# HG changeset patch # User wenzelm # Date 1122556794 -7200 # Node ID 0822bbdd6769f5d4d64967e5a8a0c681636d06ce # Parent 93772bd338716069c658197b66065e9caf2e4ac3 print_theory: const constraints; diff -r 93772bd33871 -r 0822bbdd6769 src/Pure/display.ML --- a/src/Pure/display.ML Thu Jul 28 15:19:53 2005 +0200 +++ b/src/Pure/display.ML Thu Jul 28 15:19:54 2005 +0200 @@ -186,7 +186,7 @@ val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars); - fun pretty_const (c, (ty, _)) = Pretty.block + fun pretty_const (c, ty) = Pretty.block [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty]; fun pretty_final (c, []) = Pretty.str c @@ -197,13 +197,14 @@ fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t]; val {axioms, defs, oracles} = Theory.rep_theory thy; - val {naming, syn = _, tsig, consts} = Sign.rep_sg thy; + val {naming, syn = _, tsig, consts = (consts, constraints)} = Sign.rep_sg thy; val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig; val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes); val tdecls = NameSpace.dest_table types; val arties = NameSpace.dest_table (Sign.type_space thy, arities); - val cnsts = NameSpace.extern_table consts; + val cnsts = NameSpace.extern_table consts |> map (apsnd fst); + val cnsts' = NameSpace.extern_table (#1 consts, constraints); val finals = NameSpace.extern_table (#1 consts, Defs.finals defs); val axms = NameSpace.extern_table axioms; val oras = NameSpace.extern_table oracles; @@ -219,6 +220,7 @@ Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls), Pretty.big_list "type arities:" (pretty_arities arties), Pretty.big_list "consts:" (map pretty_const cnsts), + Pretty.big_list "const constraints:" (map pretty_const cnsts'), Pretty.big_list "finals consts:" (map pretty_final finals), Pretty.big_list "axioms:" (map prt_axm axms), Pretty.strs ("oracles:" :: (map #1 oras))]