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