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