| changeset 26480 | 544cef16045b |
| parent 24783 | 5a3e336a2e37 |
| child 27226 | 5a3e5e46d977 |
--- a/src/HOL/Bali/Term.thy Sat Mar 29 19:13:58 2008 +0100 +++ b/src/HOL/Bali/Term.thy Sat Mar 29 19:14:00 2008 +0100 @@ -266,7 +266,7 @@ is_stmt :: "term \<Rightarrow> bool" "is_stmt t \<equiv> \<exists>c. t=In1r c" -ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *} +ML {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *} declare is_stmt_rews [simp]