# HG changeset patch
# User haftmann
# Date 1235322005 -3600
# Node ID 672012330c4eba51ec3cbbb5ee3ae61c57178c87
# Parent  c53242ef274ed2b97882f033e05e2f30c29e084c
subalgebra: drop arities if desired

diff -r c53242ef274e -r 672012330c4e src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Feb 22 17:33:16 2009 +0100
+++ b/src/Pure/Isar/code.ML	Sun Feb 22 18:00:05 2009 +0100
@@ -489,7 +489,7 @@
 
 fun retrieve_algebra thy operational =
   Sorts.subalgebra (Syntax.pp_global thy) operational
-    (arity_constraints thy (Sign.classes_of thy))
+    (SOME o arity_constraints thy (Sign.classes_of thy))
     (Sign.classes_of thy);
 
 in
diff -r c53242ef274e -r 672012330c4e src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sun Feb 22 17:33:16 2009 +0100
+++ b/src/Pure/sorts.ML	Sun Feb 22 18:00:05 2009 +0100
@@ -48,7 +48,7 @@
   val merge_algebra: Pretty.pp -> algebra * algebra -> algebra
   val classrels_of: algebra -> (class * class list) list
   val instances_of: algebra -> (string * class) list
-  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list)
+  val subalgebra: Pretty.pp -> (class -> bool) -> (class * string -> sort list option)
     -> algebra -> (sort -> sort) * algebra
   type class_error
   val class_error: Pretty.pp -> class_error -> string
@@ -322,8 +322,8 @@
   let
     val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes;
     fun restrict_arity tyco (c, (_, Ss)) =
-      if P c then
-        SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) (sargs (c, tyco))
+      if P c then case sargs (c, tyco)
+       of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts
           |> map restrict_sort))
       else NONE;
     val classes' = classes |> Graph.subgraph P;