--- a/src/HOL/Transitive_Closure.thy Fri May 13 23:24:06 2011 +0200
+++ b/src/HOL/Transitive_Closure.thy Fri May 13 23:58:40 2011 +0200
@@ -1027,8 +1027,8 @@
);
*}
-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))