--- a/src/HOL/Transitive_Closure.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Apr 18 17:07:01 2013 +0200
@@ -1262,11 +1262,11 @@
*}
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)))
+ map_theory_simpset (fn ctxt => ctxt
+ addSolver (mk_solver "Trancl" Trancl_Tac.trancl_tac)
+ addSolver (mk_solver "Rtrancl" Trancl_Tac.rtrancl_tac)
+ addSolver (mk_solver "Tranclp" Tranclp_Tac.trancl_tac)
+ addSolver (mk_solver "Rtranclp" Tranclp_Tac.rtrancl_tac))
*}