Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare/hoare_tac.ML
changeset 27244 af0a44372d1f
parent 26300 03def556e26e
child 27330 1af2598b5f7d 
--- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:50 2008 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 16 22:13:52 2008 +0200
@@ -112,7 +112,7 @@
              rtac CollectI i,
              dtac CollectD i,
              (TRY(split_all_tac i)) THEN_MAYBE
-             ((rename_params_tac var_names i) THEN
+             ((rename_tac var_names i) THEN
               (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
   end;
isabelle