src/HOL/Transitive_Closure.thy

       | dec _ =  NONE 
     in dec t end;
   
   end); (* struct *)
 
-simpset_ref() := simpset ()
-    addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
-    addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac));
+change_simpset (fn ss => ss
+  addSolver (mk_solver "Trancl" (fn _ => Trancl_Tac.trancl_tac))
+  addSolver (mk_solver "Rtrancl" (fn _ => Trancl_Tac.rtrancl_tac)));
 
 *}
 
 (* Optional methods