# HG changeset patch
# User haftmann
# Date 1235322992 -3600
# Node ID ace8a0847002eb89c182580f746bc9deaeb2a266
# Parent  c95e8f696b6839dad83ef6a0110d891c116da467
handle NONE case in arity function properly

diff -r c95e8f696b68 -r ace8a0847002 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);