tuned -- dynamic ML context is updated incrementally (see also e7c47fe56fbd);

--- a/src/HOL/Spec_Check/Examples.thy	Thu May 30 22:15:06 2013 +0200
+++ b/src/HOL/Spec_Check/Examples.thy	Thu May 30 22:16:33 2013 +0200
@@ -75,8 +75,8 @@
 *}
 
 
-ML {* val thy = @{theory}; *}
 ML_command {*
+val thy = @{theory};
 check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
 *}