src/HOL/Bali/Term.thy
changeset 24019 67bde7cfcf10
parent 16417 9bc16273c2d4
child 24783 5a3e336a2e37
     1.1 --- a/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:20 2007 +0200
     1.2 +++ b/src/HOL/Bali/Term.thy	Sat Jul 28 20:40:22 2007 +0200
     1.3 @@ -266,9 +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 {*
     1.8 -bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
     1.9 -*}
    1.10 +ML_setup {* bind_thms ("is_stmt_rews", sum3_instantiate @{thm is_stmt_def}) *}
    1.11  
    1.12  declare is_stmt_rews [simp]
    1.13