# HG changeset patch
# User wenzelm
# Date 1293621922 -3600
# Node ID 0bc364f772efa19ccc55f336bca31fb793008cac
# Parent  08a072ca634852a5eef558b773547fc24b75d23d
made SML/NJ happy;

diff -r 08a072ca6348 -r 0bc364f772ef 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