# HG changeset patch
# User wenzelm
# Date 1369944993 -7200
# Node ID f22d227a090c5459c9cd387d0775e9edcf963594
# Parent  3de2666b089da60944191089acdc8ca3201a12f5
tuned -- dynamic ML context is updated incrementally (see also e7c47fe56fbd);

diff -r 3de2666b089d -r f22d227a090c src/HOL/Spec_Check/Examples.thy
--- 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"
 *}