# HG changeset patch
# User haftmann
# Date 1201851146 -3600
# Node ID 9830e7ffd5749907e4bd33105f7eee8936e2c891
# Parent  4ae4ea600e8f02b05c0cfe97d6006d5f8efb5dfe
fixed term_of_sort

diff -r 4ae4ea600e8f -r 9830e7ffd574 src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Feb 01 08:32:10 2008 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Fri Feb 01 08:32:26 2008 +0100
@@ -39,8 +39,10 @@
   let
     fun classes (Const (c, _)) = [c]
       | classes (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 tm = raise TERM ("sort_of_term: bad encoding of classes", [tm]);
 
     fun sort (Const ("_topsort", _)) = []