src/HOL/Mutabelle/mutabelle_extra.ML
changeset 41409 0bc364f772ef
parent 41408 08a072ca6348
child 41491 a2ad5b824051
--- 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