src/Pure/display.ML
changeset 42358 b47d41d9f4b5
parent 39166 19efc2af3e6c
child 42359 6ca5407863ed
     1.1 --- a/src/Pure/display.ML	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -187,25 +187,25 @@
     1.4      val {restricts, reducts} = Defs.dest defs;
     1.5      val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     1.6      val {constants, constraints} = Consts.dest consts;
     1.7 -    val extern_const = Name_Space.extern (#1 constants);
     1.8 +    val extern_const = Name_Space.extern ctxt (#1 constants);
     1.9      val {classes, default, types, ...} = Type.rep_tsig tsig;
    1.10      val (class_space, class_algebra) = classes;
    1.11      val classes = Sorts.classes_of class_algebra;
    1.12      val arities = Sorts.arities_of class_algebra;
    1.13  
    1.14 -    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.15 -    val tdecls = Name_Space.dest_table types;
    1.16 -    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
    1.17 +    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
    1.18 +    val tdecls = Name_Space.dest_table ctxt types;
    1.19 +    val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities);
    1.20  
    1.21      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
    1.22 -    val cnsts = Name_Space.extern_table (#1 constants,
    1.23 +    val cnsts = Name_Space.extern_table ctxt (#1 constants,
    1.24        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
    1.25  
    1.26      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.27      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.28 -    val cnstrs = Name_Space.extern_table constraints;
    1.29 +    val cnstrs = Name_Space.extern_table ctxt constraints;
    1.30  
    1.31 -    val axms = Name_Space.extern_table axioms;
    1.32 +    val axms = Name_Space.extern_table ctxt axioms;
    1.33  
    1.34      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
    1.35        |> map (fn (lhs, rhs) =>
    1.36 @@ -225,7 +225,7 @@
    1.37        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
    1.38        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
    1.39        Pretty.big_list "axioms:" (map pretty_axm axms),
    1.40 -      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
    1.41 +      Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt),
    1.42        Pretty.big_list "definitions:"
    1.43          [pretty_finals reds0,
    1.44           Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),