src/Pure/context.ML
changeset 62819 d3ff367a16a0
parent 62663 bea354f6ff21
child 62876 507c90523113
equal deleted inserted replaced
62818:2733b240bfea 62819:d3ff367a16a0
   167     val ancestor_names = map theory_name (ancestors_of thy);
   167     val ancestor_names = map theory_name (ancestors_of thy);
   168   in rev (name :: ancestor_names) end;
   168   in rev (name :: ancestor_names) end;
   169 
   169 
   170 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   170 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   171 
   171 
   172 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
   172 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
   173 
   173 
   174 fun pretty_abbrev_thy thy =
   174 fun pretty_abbrev_thy thy =
   175   let
   175   let
   176     val names = display_names thy;
   176     val names = display_names thy;
   177     val n = length names;
   177     val n = length names;