# HG changeset patch
# User wenzelm
# Date 1369944689 -7200
# Node ID e7c47fe56fbdb9bff8a9550fa79d48816cfa6664
# Parent  65fb8cec59a54b1b3571cc90334fce75e861a5af
toplevel invocation via implicit ML compilation context;

diff -r 65fb8cec59a5 -r e7c47fe56fbd src/HOL/Spec_Check/Examples.thy
--- a/src/HOL/Spec_Check/Examples.thy	Thu May 30 22:08:01 2013 +0200
+++ b/src/HOL/Spec_Check/Examples.thy	Thu May 30 22:11:29 2013 +0200
@@ -5,11 +5,11 @@
 section {* List examples *}
 
 ML_command {*
-check_property @{context} "ALL xs. rev xs = xs";
+check_property "ALL xs. rev xs = xs";
 *}
 
 ML_command {*
-check_property @{context} "ALL xs. rev (rev xs) = xs";
+check_property "ALL xs. rev (rev xs) = xs";
 *}
 
 
@@ -17,67 +17,67 @@
 
 ML_command {*
 (* map_entry applies the function to the element *)
-check_property @{context} "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
+check_property "ALL k f xs. AList.lookup (op =) (AList.map_entry (op =) k f xs) k = Option.map f (AList.lookup (op =) xs k)";
 *}
 
 ML_command {*
 (* update always results in an entry *)
-check_property @{context} "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
+check_property "ALL k v xs. AList.defined (op =) (AList.update (op =) (k, v) xs) k";
 *}
 
 ML_command {*
 (* update always writes the value *)
-check_property @{context} "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
+check_property "ALL k v xs. AList.lookup (op =) (AList.update (op =) (k, v) xs) k = SOME v";
 *}
 
 ML_command {*
 (* default always results in an entry *)
-check_property @{context} "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
+check_property "ALL k v xs. AList.defined (op =) (AList.default (op =) (k, v) xs) k";
 *}
 
 ML_command {*
 (* delete always removes the entry *)
-check_property @{context} "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
+check_property "ALL k xs. not (AList.defined (op =) (AList.delete (op =) k xs) k)";
 *}
 
 ML_command {*
 (* default writes the entry iff it didn't exist *)
-check_property @{context} "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
+check_property "ALL k v xs. (AList.lookup (op =) (AList.default (op =) (k, v) xs) k = (if AList.defined (op =) xs k then AList.lookup (op =) xs k else SOME v))";
 *}
 
 section {* Examples on Types and Terms *}
 
 ML_command {*
-check_property @{context} "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
+check_property "ALL f g t. map_types (g o f) t = (map_types f o map_types g) t";
 *}
 
 ML_command {*
-check_property @{context} "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
+check_property "ALL f g t. map_types (f o g) t = (map_types f o map_types g) t";
 *}
 
 
 text {* One would think this holds: *}
 
 ML_command {*
-check_property @{context} "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
+check_property "ALL t ts. strip_comb (list_comb (t, ts)) = (t, ts)"
 *}
 
 text {* But it only holds with this precondition: *}
 
 ML_command {*
-check_property @{context} "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
+check_property "ALL t ts. case t of _ $ _ => true | _ => strip_comb (list_comb (t, ts)) = (t, ts)"
 *}
 
 section {* Some surprises *}
 
 ML_command {*
-check_property @{context} "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
+check_property "ALL Ts t. type_of1 (Ts, t) = fastype_of1 (Ts, t)"
 *}
 
 
 ML {* val thy = @{theory}; *}
 ML_command {*
-check_property @{context} "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
+check_property "ALL t u. if Pattern.matches thy (t, u) then Term.could_unify (t, u) else true"
 *}
 
 end
diff -r 65fb8cec59a5 -r e7c47fe56fbd src/HOL/Spec_Check/README
--- 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
 
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;