changeset 46709 | 65a9b30bff00 |
parent 45740 | 132a3e1c0fe5 |
child 47108 | 2a1953f0d20d |
--- a/src/HOL/Tools/lin_arith.ML Mon Feb 27 15:48:02 2012 +0100 +++ b/src/HOL/Tools/lin_arith.ML Mon Feb 27 16:05:51 2012 +0100 @@ -901,7 +901,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.prems_lin_arith_tac))); val global_setup = Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))