src/HOL/Statespace/state_space.ML

     val raw_parent_comps = (List.concat (map (parent_components thy) parents'));
     fun check_type (n,T) =
           (case distinct (snd_eq) (filter (curry fst_eq (n,T)) raw_parent_comps) of
              []  => []
            | [_] => []
-           | rs  => ["Different types for component " ^ n ^": " ^ commas
-                       (map (Pretty.string_of o Display.pretty_ctyp o ctyp_of thy o snd) rs)])
+           | rs  => ["Different types for component " ^ n ^": " ^
+                commas (map (Syntax.string_of_typ ctxt o snd) rs)])
 
     val err_dup_types = List.concat (map check_type (duplicates fst_eq raw_parent_comps))
 
     val parent_comps = distinct (fst_eq) raw_parent_comps;
     val all_comps = parent_comps @ comps';