print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
authorwenzelm
Sun Sep 30 16:20:35 2007 +0200 (2007-09-30)
changeset 24774bc31c318e673
parent 24773 ec3a04e6f1a9
child 24775 4f86d3384111
print_theory: observe Markup.internal_property of consts, discontinued special treatment of internal names elsewhere;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Sun Sep 30 16:20:35 2007 +0200
     1.2 +++ b/src/Pure/display.ML	Sun Sep 30 16:20:35 2007 +0200
     1.3 @@ -209,23 +209,25 @@
     1.4      val (class_space, class_algebra) = classes;
     1.5      val {classes, arities} = Sorts.rep_algebra class_algebra;
     1.6  
     1.7 -    fun prune xs = if verbose then xs else filter_out (can Name.dest_internal o fst) xs;
     1.8 -    fun prune' xs = if verbose then xs else filter_out (can Name.dest_internal o fst o fst) xs;
     1.9 -    fun dest_table tab = prune (NameSpace.dest_table tab);
    1.10 -    fun extern_table tab = prune (NameSpace.extern_table tab);
    1.11 +    val clsses = NameSpace.dest_table (class_space, Symtab.make (Graph.dest classes));
    1.12 +    val tdecls = NameSpace.dest_table types;
    1.13 +    val arties = NameSpace.dest_table (Sign.type_space thy, arities);
    1.14  
    1.15 -    val clsses = dest_table (class_space, Symtab.make (Graph.dest classes));
    1.16 -    val tdecls = dest_table types;
    1.17 -    val arties = dest_table (Sign.type_space thy, arities);
    1.18 -    val cnsts = extern_table constants;
    1.19 +    fun prune_const c = not verbose andalso
    1.20 +      member (op =) (Consts.the_tags consts c) Markup.property_internal;
    1.21 +    val cnsts = NameSpace.extern_table (#1 constants,
    1.22 +      Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
    1.23 +
    1.24      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
    1.25      val abbrevs = map_filter (fn (c, (ty, SOME (t, _))) => SOME (c, (ty, t)) | _ => NONE) cnsts;
    1.26 -    val cnstrs = extern_table constraints;
    1.27 -    val axms = extern_table axioms;
    1.28 -    val oras = extern_table oracles;
    1.29 +    val cnstrs = NameSpace.extern_table constraints;
    1.30  
    1.31 -    val (reds0, (reds1, reds2)) = prune' reducts |> map (fn (lhs, rhs) =>
    1.32 -        (apfst extern_const lhs, map (apfst extern_const) (prune rhs)))
    1.33 +    val axms = NameSpace.extern_table axioms;
    1.34 +    val oras = NameSpace.extern_table oracles;
    1.35 +
    1.36 +    val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
    1.37 +      |> map (fn (lhs, rhs) =>
    1.38 +        (apfst extern_const lhs, map (apfst extern_const) (filter_out (prune_const o fst) rhs)))
    1.39        |> sort_wrt (#1 o #1)
    1.40        |> List.partition (null o #2)
    1.41        ||> List.partition (Defs.plain_args o #2 o #1);