1.1 --- a/src/HOL/Hoare/Hoare.ML	Sat Mar 25 12:59:31 2000 +0100
     1.2 +++ b/src/HOL/Hoare/Hoare.ML	Sat Mar 25 13:00:44 2000 +0100
     1.3 @@ -163,7 +163,7 @@
     1.4            (EVERY [rtac subsetI i, 
     1.5                    rtac CollectI i,
     1.6                    dtac CollectD i,
     1.7 -                  (TRY(split_all_tac i)) THEN_MAYBE 
     1.8 +                  (TRY(split_all_tac i)) THEN_MAYBE
     1.9                    ((rename_tac var_string i) THEN
    1.10                     (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
    1.11        end;
    1.12 @@ -179,7 +179,8 @@
    1.13  fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
    1.14  
    1.15  fun BasicSimpTac tac =
    1.16 -  simp_tac (HOL_basic_ss addsimps [mem_Collect_eq,split])
    1.17 +  simp_tac
    1.18 +    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
    1.19    THEN_MAYBE' MaxSimpTac tac;
    1.20  
    1.21  (** HoareRuleTac **)
    1.22 @@ -217,4 +218,4 @@
    1.23  
    1.24  val hoare_setup =
    1.25   [Method.add_methods
    1.26 -  [("hoare", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];
    1.27 +  [("hoare_vcg", Method.no_args hoare_method, "verification condition generator for Hoare logic")]];