changeset 43596 | 78211f66cf8d |
parent 43595 | 7ae4a23b5be6 |
child 43609 | 20760e3608fa |
--- a/src/HOL/Tools/lin_arith.ML Wed Jun 29 18:12:34 2011 +0200 +++ b/src/HOL/Tools/lin_arith.ML Wed Jun 29 20:39:41 2011 +0200 @@ -895,7 +895,7 @@ val setup = init_arith_data #> Simplifier.map_ss (fn ss => ss - addSolver (mk_solver' "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); + addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))); val global_setup = Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))