--- a/src/HOL/ex/Numeral_Representation.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/ex/Numeral_Representation.thy Thu Apr 18 17:07:01 2013 +0200
@@ -817,7 +817,7 @@
ML {*
structure Semiring_Times_Assoc_Data : ASSOC_FOLD_DATA =
struct
- val assoc_ss = HOL_ss addsimps @{thms mult_ac_numeral}
+ val assoc_ss = simpset_of (put_simpset HOL_ss @{context} addsimps @{thms mult_ac_numeral})
val eq_reflection = eq_reflection
fun is_numeral (Const(@{const_name of_num}, _) $ _) = true
| is_numeral _ = false;