print_theory: const abbreviations;
authorwenzelm
Mon Feb 06 20:59:03 2006 +0100 (2006-02-06)
changeset 18936647528660980
parent 18935 f22be3d61ed5
child 18937 0eb35519f0f3
print_theory: const abbreviations;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Mon Feb 06 20:59:02 2006 +0100
     1.2 +++ b/src/Pure/display.ML	Mon Feb 06 20:59:03 2006 +0100
     1.3 @@ -161,6 +161,7 @@
     1.4      fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
     1.5      val prt_typ_no_tvars = prt_typ o Type.freeze_type;
     1.6      fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
     1.7 +    val prt_term_no_vars = prt_term o Logic.unvarify;
     1.8  
     1.9      fun pretty_classrel (c, []) = prt_cls c
    1.10        | pretty_classrel (c, cs) = Pretty.block
    1.11 @@ -189,21 +190,22 @@
    1.12  
    1.13      val pretty_arities = List.concat o map (fn (t, ars) => map (prt_arity t) ars);
    1.14  
    1.15 -    fun pretty_const (c, ty) = Pretty.block
    1.16 -      [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
    1.17 +    fun pretty_const (c, (ty, rhs)) = Pretty.block
    1.18 +      ([Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty] @
    1.19 +        (case rhs of NONE => [] | SOME t => [Pretty.str " ==", Pretty.brk 1, prt_term_no_vars t]));
    1.20  
    1.21 -    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
    1.22 +    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term_no_vars t];
    1.23  
    1.24      val {axioms, defs = _, oracles} = Theory.rep_theory thy;
    1.25      val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
    1.26 -    val {declarations, constraints} = Consts.dest consts;
    1.27 +    val {constants, constraints} = Consts.dest consts;
    1.28      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.29  
    1.30      val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
    1.31      val tdecls = NameSpace.dest_table types;
    1.32      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.33 -    val cnsts = NameSpace.extern_table declarations;
    1.34 -    val cnsts' = NameSpace.extern_table constraints;
    1.35 +    val cnsts = NameSpace.extern_table constants;
    1.36 +    val cnstrs = NameSpace.extern_table constraints |> map (apsnd (rpair NONE));
    1.37      val axms = NameSpace.extern_table axioms;
    1.38      val oras = NameSpace.extern_table oracles;
    1.39    in
    1.40 @@ -218,7 +220,7 @@
    1.41        Pretty.big_list "logical types:" (List.mapPartial (pretty_type false) tdecls),
    1.42        Pretty.big_list "type arities:" (pretty_arities arties),
    1.43        Pretty.big_list "consts:" (map pretty_const cnsts),
    1.44 -      Pretty.big_list "const constraints:" (map pretty_const cnsts'),
    1.45 +      Pretty.big_list "const constraints:" (map pretty_const cnstrs),
    1.46        Pretty.big_list "axioms:" (map prt_axm axms),
    1.47        Pretty.strs ("oracles:" :: (map #1 oras))]
    1.48    end;