src/Pure/Isar/code.ML
changeset 30060 672012330c4e
parent 30023 55954f726043
child 30076 f3043dafef5f
     1.1 --- a/src/Pure/Isar/code.ML	Sun Feb 22 17:33:16 2009 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sun Feb 22 18:00:05 2009 +0100
     1.3 @@ -489,7 +489,7 @@
     1.4  
     1.5  fun retrieve_algebra thy operational =
     1.6    Sorts.subalgebra (Syntax.pp_global thy) operational
     1.7 -    (arity_constraints thy (Sign.classes_of thy))
     1.8 +    (SOME o arity_constraints thy (Sign.classes_of thy))
     1.9      (Sign.classes_of thy);
    1.10  
    1.11  in