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