src/HOL/Mutabelle/mutabelle_extra.ML

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:22:38 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Dec 29 12:25:22 2010 +0100
@@ -330,7 +330,7 @@
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Mutabelle.all_unconcealed_thms_of thy)))
 
-val count = length oo filter o equal
+fun count x = (length oo filter o equal) x
 
 fun cpu_time description f =
   let