# HG changeset patch
# User wenzelm
# Date 1175638268 -7200
# Node ID 6e56ff1a22ebf65798b8f87e4d10a84a797bcd8d
# Parent  b0eb5652f210e57f0ce05ea0aac3ca1582917b8a
eliminated obsolete rename_tac;

diff -r b0eb5652f210 -r 6e56ff1a22eb src/HOL/Hoare/hoare.ML
--- 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 **)
diff -r b0eb5652f210 -r 6e56ff1a22eb src/HOL/Hoare/hoareAbort.ML
--- a/src/HOL/Hoare/hoareAbort.ML	Wed Apr 04 00:11:03 2007 +0200
+++ b/src/HOL/Hoare/hoareAbort.ML	Wed Apr 04 00:11:08 2007 +0200
@@ -81,7 +81,7 @@
                            Free ("P",varsT --> boolT) $ Bound 0));
                    val impl = implies $ (Mset_incl big_Collect) $ 
                                           (Mset_incl small_Collect);
-   in Goal.prove (ProofContext.init (Thm.sign_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
+   in Goal.prove (ProofContext.init (Thm.theory_of_thm thm)) ["Mset", "P"] [] impl (K (CLASET' blast_tac 1)) end;
 
 end;
 
@@ -117,18 +117,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 **)