# HG changeset patch
# User wenzelm
# Date 953985644 -3600
# Node ID 142065da303db32377cbd1da7a869d58df768514
# Parent  7d79d2473b5e28520888409cba7bd5c505ce9d03
addsimprocs [record_simproc];

diff -r 7d79d2473b5e -r 142065da303d src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Sat Mar 25 12:59:31 2000 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Sat Mar 25 13:00:44 2000 +0100
@@ -163,7 +163,7 @@
           (EVERY [rtac subsetI i, 
                   rtac CollectI i,
                   dtac CollectD i,
-                  (TRY(split_all_tac i)) THEN_MAYBE 
+                  (TRY(split_all_tac i)) THEN_MAYBE
                   ((rename_tac var_string i) THEN
                    (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
       end;
@@ -179,7 +179,8 @@
 fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
 
 fun BasicSimpTac tac =
-  simp_tac (HOL_basic_ss addsimps [mem_Collect_eq,split])
+  simp_tac
+    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
   THEN_MAYBE' MaxSimpTac tac;
 
 (** HoareRuleTac **)
@@ -217,4 +218,4 @@
 
 val hoare_setup =
  [Method.add_methods
-  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];
+  [("hoare_vcg", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];