--- a/src/HOL/Spec_Check/README	Thu May 30 22:08:01 2013 +0200
+++ b/src/HOL/Spec_Check/README	Thu May 30 22:11:29 2013 +0200
@@ -9,8 +9,8 @@
 
   - Import Spec_Check.thy in your development
   - Look at examples in Examples.thy
-  - write specifications with the ML function
-      Spec_Check.check_property @{context} "ALL x. P x"
+  - write specifications with the ML invocation
+      check_property "ALL x. P x"
 
 Notes