changeset 42795 | 66fcc9882784 |
parent 42793 | 88bee9f6eec7 |
child 43324 | 2b47822868e4 |
--- a/src/HOL/Tools/record.ML Fri May 13 23:24:06 2011 +0200 +++ b/src/HOL/Tools/record.ML Fri May 13 23:58:40 2011 +0200 @@ -2508,8 +2508,7 @@ val setup = Sign.add_trfuns ([], parse_translation, [], []) #> Sign.add_advanced_trfuns ([], advanced_parse_translation, [], []) #> - Simplifier.map_simpset (fn ss => - ss addsimprocs [simproc, upd_simproc, eq_simproc]); + Simplifier.map_simpset_global (fn ss => ss addsimprocs [simproc, upd_simproc, eq_simproc]); (* outer syntax *)