src/HOL/HOL.thy

 use "simpdata.ML"
 ML {* open Simpdata *}
 
 setup {*
   Simplifier.method_setup Splitter.split_modifiers
-  #> (fn thy => (change_simpset_of thy (fn _ => Simpdata.simpset_simprocs); thy))
+  #> Simplifier.map_simpset (K Simpdata.simpset_simprocs)
   #> Splitter.setup
-  #> Clasimp.setup
+  #> clasimp_setup
   #> EqSubst.setup
 *}
 
 text {* Simproc for proving @{text "(y = x) == False"} from premise @{text "~(x = y)"}: *}