src/Pure/display.ML
changeset 33095 bbd52d2f8696
parent 33092 c859019d3ac5
child 33158 6e3dc0ba2b06
     1.1 --- a/src/Pure/display.ML	Sat Oct 24 19:24:50 2009 +0200
     1.2 +++ b/src/Pure/display.ML	Sat Oct 24 19:47:37 2009 +0200
     1.3 @@ -179,25 +179,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 = NameSpace.extern (#1 constants);
     1.8 +    val extern_const = Name_Space.extern (#1 constants);
     1.9      val {classes, default, types, ...} = Type.rep_tsig tsig;
    1.10      val (class_space, class_algebra) = classes;
    1.11      val {classes, arities} = Sorts.rep_algebra class_algebra;
    1.12  
    1.13 -    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.14 -    val tdecls = NameSpace.dest_table types;
    1.15 -    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.16 +    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.17 +    val tdecls = Name_Space.dest_table types;
    1.18 +    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
    1.19  
    1.20      fun prune_const c = not verbose andalso
    1.21        member (op =) (Consts.the_tags consts c) Markup.property_internal;
    1.22 -    val cnsts = NameSpace.extern_table (#1 constants,
    1.23 +    val cnsts = Name_Space.extern_table (#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 = NameSpace.extern_table constraints;
    1.29 +    val cnstrs = Name_Space.extern_table constraints;
    1.30  
    1.31 -    val axms = NameSpace.extern_table axioms;
    1.32 +    val axms = Name_Space.extern_table axioms;
    1.33  
    1.34      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
    1.35        |> map (fn (lhs, rhs) =>