src/HOL/Bali/Term.thy

--- a/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:20 2007 +0200
+++ b/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:22 2007 +0200
@@ -266,9 +266,7 @@
   is_stmt :: "term \<Rightarrow> bool"
  "is_stmt t \<equiv> \<exists>c. t=In1r c"
 
-ML {*
-bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
-*}
+ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
 
 declare is_stmt_rews [simp]