diff -r 3a2efce3e992 -r 544cef16045b src/HOL/Bali/Example.thy --- a/src/HOL/Bali/Example.thy Sat Mar 29 19:13:58 2008 +0100 +++ b/src/HOL/Bali/Example.thy Sat Mar 29 19:14:00 2008 +0100 @@ -894,7 +894,7 @@ declare member_is_static_simp [simp] declare wt.Skip [rule del] wt.Init [rule del] -ML_setup {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *} +ML {* bind_thms ("wt_intros", map (rewrite_rule @{thms id_def}) @{thms wt.intros}) *} lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros lemmas daIs = assigned.select_convs da_Skip da_NewC da_Lit da_Super da.intros @@ -1192,7 +1192,7 @@ declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] Base_foo_defs [simp] -ML_setup {* bind_thms ("eval_intros", map +ML {* bind_thms ("eval_intros", map (simplify (@{simpset} delsimps @{thms Skip_eq} addsimps @{thms lvar_def}) o rewrite_rule [@{thm assign_def}, @{thm Let_def}]) @{thms eval.intros}) *}