# HG changeset patch
# User wenzelm
# Date 1202123588 -3600
# Node ID a27710a07d10bc8d757ac9d32fa5a64e2f42b7ef
# Parent  55a02586776d964fd0755dafd6724aa5dcf18ab7
*** MESSAGE REFERS TO 1.29 and 1.44 ***
sort_of_term: be permissive about _class *output* markers, to allow print translations invoke this function as well;

diff -r 55a02586776d -r a27710a07d10 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Mon Feb 04 10:52:40 2008 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Mon Feb 04 12:13:08 2008 +0100
@@ -39,16 +39,16 @@
   let
     fun classes (Const (c, _)) = [c]
       | classes (Free (c, _)) = [c]
-      | classes (Const ("_class",_) $ Free (c, _)) = [c]
+      | classes (Const ("_class", _) $ Free (c, _)) = [c]
       | classes (Const ("_classes", _) $ Const (c, _) $ cs) = c :: classes cs
       | classes (Const ("_classes", _) $ Free (c, _) $ cs) = c :: classes cs
-      | classes (Const ("_classes", _) $ (Const ("_class",_) $ Free (c, _)) $ cs) = c :: classes cs
+      | classes (Const ("_classes", _) $ (Const ("_class", _) $ Free (c, _)) $ cs) = c :: classes cs
       | classes tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
 
     fun sort (Const ("_topsort", _)) = []
       | sort (Const (c, _)) = [c]
       | sort (Free (c, _)) = [c]
-      | sort (Const ("_class",_) $ Free (c, _)) = [c]
+      | sort (Const ("_class", _) $ Free (c, _)) = [c]
       | sort (Const ("_sort", _) $ cs) = classes cs
       | sort tm = raise TERM ("sort_of_term: bad encoding of sort", [tm]);
   in map_sort (sort tm) end;