changeset 26496 | 49ae9456eba9 |
parent 25408 | 156f6f7082b8 |
child 27099 | 2a91d9575935 |
--- a/src/HOL/Statespace/state_fun.ML Sat Mar 29 19:24:57 2008 +0100 +++ b/src/HOL/Statespace/state_fun.ML Sat Mar 29 22:55:49 2008 +0100 @@ -381,8 +381,7 @@ | _ => (lookup_ss addsimps [thm], ex_lookup_ss)) fun activate_simprocs ctxt = if simprocs_active then ctxt - else StateSpace.change_simpset - (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt + else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt val ctxt' = ctxt