src/HOL/Hoare/hoare_tac.ML
changeset 27244 af0a44372d1f
parent 26300 03def556e26e
child 27330 1af2598b5f7d
     1.1 --- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:50 2008 +0200
     1.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:52 2008 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4               rtac CollectI i,
     1.5               dtac CollectD i,
     1.6               (TRY(split_all_tac i)) THEN_MAYBE
     1.7 -             ((rename_params_tac var_names i) THEN
     1.8 +             ((rename_tac var_names i) THEN
     1.9                (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
    1.10    end;
    1.11