diff -r 65fb8cec59a5 -r e7c47fe56fbd src/HOL/Spec_Check/spec_check.ML
--- a/src/HOL/Spec_Check/spec_check.ML	Thu May 30 22:08:01 2013 +0200
+++ b/src/HOL/Spec_Check/spec_check.ML	Thu May 30 22:11:29 2013 +0200
@@ -188,5 +188,5 @@
 
 end;
 
-val check_property = Spec_Check.check_property;
+fun check_property s = Spec_Check.check_property (ML_Context.the_local_context ()) s;