diff -r 5a1b299fe4af -r 17874d43d3b3 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sat Feb 24 17:21:35 2018 +0100 +++ b/src/Pure/pure_thy.ML Sun Feb 25 12:59:08 2018 +0100 @@ -105,6 +105,7 @@ ("", typ "class_name => sort", Mixfix.mixfix "_"), ("_class_name", typ "id => class_name", Mixfix.mixfix "_"), ("_class_name", typ "longid => class_name", Mixfix.mixfix "_"), + ("_dummy_sort", typ "sort", Mixfix.mixfix "'_"), ("_topsort", typ "sort", Mixfix.mixfix "{}"), ("_sort", typ "classes => sort", Mixfix.mixfix "{_}"), ("", typ "class_name => classes", Mixfix.mixfix "_"),