quote tag arguments;
authorwenzelm
Thu Mar 09 22:57:39 2000 +0100 (2000-03-09)
changeset 840284ff2d1f9a2c
parent 8401 50d5f4402305
child 8403 a8a0411a8e8c
quote tag arguments;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Thu Mar 09 22:57:13 2000 +0100
     1.2 +++ b/src/Pure/display.ML	Thu Mar 09 22:57:39 2000 +0100
     1.3 @@ -46,7 +46,7 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun pretty_tag (name, args) = Pretty.strs (name :: args);
     1.8 +fun pretty_tag (name, args) = Pretty.strs (name :: map quote args);
     1.9  val pretty_tags = Pretty.list "[" "]" o map pretty_tag;
    1.10  
    1.11  fun is_oracle (Thm.Oracle _) = true
    1.12 @@ -183,7 +183,8 @@
    1.13  
    1.14      fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
    1.15        | pretty_witness (Some (T, S)) = Pretty.block
    1.16 -          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ T, Pretty.brk 1, prt_sort S];
    1.17 +          [Pretty.str "universal non-emptiness witness:", Pretty.brk 1, prt_typ T,
    1.18 +            Pretty.brk 1, prt_sort S];
    1.19  
    1.20      fun pretty_abbr (t, (vs, rhs)) = Pretty.block
    1.21        [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
    1.22 @@ -206,13 +207,15 @@
    1.23      Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
    1.24      Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
    1.25      Pretty.writeln (pretty_classes classes);
    1.26 -    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)));
    1.27 +    Pretty.writeln (Pretty.big_list "class relation:"
    1.28 +      (map pretty_classrel (Symtab.dest classrel)));
    1.29      Pretty.writeln (pretty_default default);
    1.30      Pretty.writeln (pretty_log_types log_types);
    1.31      Pretty.writeln (pretty_witness univ_witness);
    1.32      Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
    1.33      Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
    1.34 -    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))));
    1.35 +    Pretty.writeln (Pretty.big_list "type arities:"
    1.36 +      (flat (map pretty_arities (Symtab.dest arities))));
    1.37      Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
    1.38    end;
    1.39