src/HOL/Tools/record.ML
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 *)