| changeset 52260 | e7c47fe56fbd |
| parent 52259 | 65fb8cec59a5 |
| child 52263 | 320c86e50f84 |
--- 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;