src/HOL/Transitive_Closure.thy

     in dec t end
     | decomp _ = NONE;
 );
 *}
 
-declaration {* fn _ =>
-  Simplifier.map_ss (fn ss => ss
+setup {*
+  Simplifier.map_simpset_global (fn ss => ss
     addSolver (mk_solver' "Trancl" (Trancl_Tac.trancl_tac o Simplifier.the_context))
     addSolver (mk_solver' "Rtrancl" (Trancl_Tac.rtrancl_tac o Simplifier.the_context))
     addSolver (mk_solver' "Tranclp" (Tranclp_Tac.trancl_tac o Simplifier.the_context))
     addSolver (mk_solver' "Rtranclp" (Tranclp_Tac.rtrancl_tac o Simplifier.the_context)))
 *}