--- a/src/HOL/Hoare/hoare.ML Wed Apr 04 00:11:03 2007 +0200
+++ b/src/HOL/Hoare/hoare.ML Wed Apr 04 00:11:08 2007 +0200
@@ -116,18 +116,16 @@
(** simplification done by (split_all_tac) **)
(*****************************************************************************)
-fun set2pred i thm = let fun mk_string [] = ""
- | mk_string (x::xs) = x^" "^mk_string xs;
- val vars=get_vars(thm);
- val var_string = mk_string (map (fst o dest_Free) vars);
- in ((before_set2pred_simp_tac i) THEN_MAYBE
- (EVERY [rtac subsetI i,
- rtac CollectI i,
- dtac CollectD i,
- (TRY(split_all_tac i)) THEN_MAYBE
- ((rename_tac var_string i) THEN
- (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
- end;
+fun set2pred i thm =
+ let val var_names = map (fst o dest_Free) (get_vars thm) in
+ ((before_set2pred_simp_tac i) THEN_MAYBE
+ (EVERY [rtac subsetI i,
+ rtac CollectI i,
+ dtac CollectD i,
+ (TRY(split_all_tac i)) THEN_MAYBE
+ ((rename_params_tac var_names i) THEN
+ (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
+ end;
(*****************************************************************************)
(** BasicSimpTac is called to simplify all verification conditions. It does **)