src/HOL/Mutabelle/mutabelle.ML

--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Apr 20 16:18:47 2011 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Apr 20 16:49:52 2011 +0200
@@ -76,7 +76,7 @@
    val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
    val consts = Symtab.dest const_table
  in
-   List.mapPartial (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
+   map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
      (filter_out (fn (s, _) => Name_Space.is_concealed namespace s) consts)
  end;