--- a/src/Pure/Syntax/syntax_phases.ML Sat Feb 24 17:21:35 2018 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Sun Feb 25 12:59:08 2018 +0100
@@ -106,7 +106,8 @@
| classes (Const ("_classes", _) $ Const (s, _) $ cs) = class s :: classes cs
| classes _ = err ();
- fun sort (Const ("_topsort", _)) = []
+ fun sort (Const ("_dummy_sort", _)) = dummyS
+ | sort (Const ("_topsort", _)) = []
| sort (Const ("_sort", _) $ cs) = classes cs
| sort (Const (s, _)) = [class s]
| sort _ = err ();
@@ -506,10 +507,12 @@
fun classes [c] = class c
| classes (c :: cs) = Syntax.const "_classes" $ class c $ classes cs;
in
- (case S of
- [] => Syntax.const "_topsort"
- | [c] => class c
- | cs => Syntax.const "_sort" $ classes cs)
+ if S = dummyS then Syntax.const "_dummy_sort"
+ else
+ (case S of
+ [] => Syntax.const "_topsort"
+ | [c] => class c
+ | cs => Syntax.const "_sort" $ classes cs)
end;