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