src/Pure/display.ML
changeset 14178 14a12da7288e
parent 13658 c9ad3e64ddcf
child 14223 0ee05eef881b
equal deleted inserted replaced
14177:06b19a7e675a 14178:14a12da7288e
   336       (if ! show_consts then pretty_consts prop else []) @
   336       (if ! show_consts then pretty_consts prop else []) @
   337       (if types then pretty_vars prop else []) @
   337       (if types then pretty_vars prop else []) @
   338       (if sorts then pretty_varsT prop else []);
   338       (if sorts then pretty_varsT prop else []);
   339   in
   339   in
   340     setmp show_no_free_types true
   340     setmp show_no_free_types true
   341       (setmp show_types (! show_types orelse ! show_sorts)
   341       (setmp show_types (! show_types orelse ! show_sorts orelse ! show_all_types)
   342         (setmp show_sorts false pretty_gs))
   342         (setmp show_sorts false pretty_gs))
   343    (! show_types orelse ! show_sorts, ! show_sorts)
   343    (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts)
   344   end;
   344   end;
   345 
   345 
   346 fun pretty_goals_marker bg n th =
   346 fun pretty_goals_marker bg n th =
   347   let val sg = Thm.sign_of_thm th in
   347   let val sg = Thm.sign_of_thm th in
   348     pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg)
   348     pretty_goals_aux (Sign.pretty_sort sg, Sign.pretty_typ sg, Sign.pretty_term sg)