1.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Wed May 26 16:28:55 2010 +0200
     1.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed May 26 16:31:44 2010 +0200
     1.3 @@ -228,7 +228,7 @@
     1.4        EVERY [
     1.5          REPEAT (etac thin_rl i),
     1.6          cut_facts_tac (mk_lam_defs defs) i,
     1.7 -        full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) i,
     1.8 +        full_simp_tac (Mucke_ss delsimps [not_iff, @{thm split_part}]) i,
     1.9          move_mus i, call_mucke_tac i,atac i,
    1.10          REPEAT (rtac refl i)] state);
    1.11  *}