handle NONE case in arity function properly
authorhaftmann
Sun, 22 Feb 2009 18:16:32 +0100
changeset 30062 ace8a0847002
parent 30061 c95e8f696b68
child 30063 e7723cb4b2a6
child 30068 eb9bdc4292be
handle NONE case in arity function properly
src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Feb 22 18:02:21 2009 +0100
+++ b/src/Pure/sorts.ML	Sun Feb 22 18:16:32 2009 +0100
@@ -325,6 +325,7 @@
       if P c then case sargs (c, tyco)
        of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
           |> map restrict_sort))
+        | NONE => NONE
       else NONE;
     val classes' = classes |> Graph.subgraph P;
     val arities' = arities |> Symtab.map' (map_filter o restrict_arity);