1.1 --- a/src/HOL/Fun.thy	Wed Mar 19 22:47:39 2008 +0100
     1.2 +++ b/src/HOL/Fun.thy	Wed Mar 19 22:50:42 2008 +0100
     1.3 @@ -532,7 +532,7 @@
     1.4  subsection {* ML legacy bindings *} 
     1.5  
     1.6  ML {*
     1.7 -val set_cs = claset() delrules [equalityI]
     1.8 +val set_cs = @{claset} delrules [@{thm equalityI}]
     1.9  *}
    1.10  
    1.11  ML {*