| changeset 38012 | 3ca193a6ae5a |
| parent 37677 | c5a8b612e571 |
| child 41449 | 7339f0e7c513 |
--- a/src/HOL/Hoare/hoare_tac.ML Mon Jul 26 14:44:07 2010 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Tue Jul 27 17:09:35 2010 +0200 @@ -125,7 +125,7 @@ fun BasicSimpTac var_names tac = simp_tac - (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [record_simproc]) + (HOL_basic_ss addsimps [mem_Collect_eq, @{thm split_conv}] addsimprocs [Record.simproc]) THEN_MAYBE' MaxSimpTac var_names tac;