--- a/src/Pure/display.ML Tue Mar 11 13:58:22 2014 +0100
+++ b/src/Pure/display.ML Tue Mar 11 14:28:39 2014 +0100
@@ -157,22 +157,24 @@
val arities = Sorts.arities_of class_algebra;
val clsses =
- Name_Space.dest_table' ctxt class_space
- (Symtab.make (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes)))
+ Name_Space.extern_entries ctxt class_space
+ (map (fn ((c, _), cs) => (c, Sign.minimize_sort thy cs)) (Graph.dest classes))
|> map (apfst #1);
- val tdecls = Name_Space.dest_table ctxt types |> map (apfst #1);
- val arties = Name_Space.dest_table' ctxt (Type.type_space tsig) arities |> map (apfst #1);
+ val tdecls = Name_Space.extern_table ctxt types |> map (apfst #1);
+ val arties =
+ Name_Space.extern_entries ctxt (Type.type_space tsig) (Symtab.dest arities)
+ |> map (apfst #1);
fun prune_const c = not verbose andalso Consts.is_concealed consts c;
val cnsts =
- Name_Space.extern_table' ctxt const_space
- (Symtab.make (filter_out (prune_const o fst) (Symtab.dest constants)));
+ Name_Space.markup_entries ctxt const_space
+ (filter_out (prune_const o fst) (Symtab.dest constants));
val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
- val cnstrs = Name_Space.extern_table' ctxt const_space constraints;
+ val cnstrs = Name_Space.markup_entries ctxt const_space (Symtab.dest constraints);
- val axms = Name_Space.extern_table ctxt (Theory.axiom_table thy);
+ val axms = Name_Space.markup_table ctxt (Theory.axiom_table thy);
val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
|> map (fn (lhs, rhs) =>