--- a/src/HOL/Mutabelle/mutabelle.ML Wed Mar 12 14:23:26 2014 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Wed Mar 12 14:37:14 2014 +0100
@@ -33,10 +33,9 @@
fun consts_of thy =
let
val {const_space, constants, ...} = Consts.dest (Sign.consts_of thy)
- val consts = Symtab.dest constants
in
map_filter (fn (s, (T, NONE)) => SOME (s, T) | _ => NONE)
- (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) consts)
+ (filter_out (fn (s, _) => Name_Space.is_concealed const_space s) constants)
end;