src/Pure/display.ML
changeset 18061 972e3d554eb8
parent 17995 8b9c6af78a67
child 18936 647528660980
     1.1 --- a/src/Pure/display.ML	Wed Nov 02 14:46:56 2005 +0100
     1.2 +++ b/src/Pure/display.ML	Wed Nov 02 14:46:57 2005 +0100
     1.3 @@ -195,14 +195,15 @@
     1.4      fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1, prt_term t];
     1.5  
     1.6      val {axioms, defs = _, oracles} = Theory.rep_theory thy;
     1.7 -    val {naming, syn = _, tsig, consts = (consts, constraints)} = Sign.rep_sg thy;
     1.8 +    val {naming, syn = _, tsig, consts} = Sign.rep_sg thy;
     1.9 +    val {declarations, constraints} = Consts.dest consts;
    1.10      val {classes, default, types, arities, log_types = _, witness} = Type.rep_tsig tsig;
    1.11  
    1.12      val clsses = NameSpace.dest_table (apsnd (Symtab.make o Graph.dest) classes);
    1.13      val tdecls = NameSpace.dest_table types;
    1.14      val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.15 -    val cnsts = NameSpace.extern_table consts |> map (apsnd (fst o fst));
    1.16 -    val cnsts' = NameSpace.extern_table (#1 consts, constraints);
    1.17 +    val cnsts = NameSpace.extern_table declarations;
    1.18 +    val cnsts' = NameSpace.extern_table constraints;
    1.19      val axms = NameSpace.extern_table axioms;
    1.20      val oras = NameSpace.extern_table oracles;
    1.21    in