Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed term_of_sort
authorhaftmann
Fri, 01 Feb 2008 08:32:26 +0100
changeset 26031 9830e7ffd574
parent 26030 4ae4ea600e8f
child 26032 377b7aa0b5b5
fixed term_of_sort
src/Pure/Syntax/type_ext.ML file | annotate | diff | comparison | revisions 
--- 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", _)) = []
isabelle