| changeset 51717 | 9e7d1c139569 |
| parent 48659 | 40a87b4dac19 |
| child 58880 | 0baae4311a9f |
--- a/src/HOL/HOLCF/Tr.thy Tue Apr 16 17:54:14 2013 +0200 +++ b/src/HOL/HOLCF/Tr.thy Thu Apr 18 17:07:01 2013 +0200 @@ -150,9 +150,10 @@ apply (simp_all) done +(* FIXME unused!? *) ML {* -val split_If_tac = - simp_tac (HOL_basic_ss addsimps [@{thm If2_def} RS sym]) +fun split_If_tac ctxt = + simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm If2_def} RS sym]) THEN' (split_tac [@{thm split_If2}]) *}