--- a/src/HOL/arith_data.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/arith_data.ML Sat Oct 06 00:02:46 2001 +0200
@@ -438,7 +438,7 @@
[Simplifier.change_simpset_of (op addSolver)
(mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
- Method.add_methods [("arith", (arith_method o # 2) oo Method.syntax Args.bang_facts,
+ Method.add_methods [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
"decide linear arithmethic")],
Attrib.add_attributes [("arith_split",
(Attrib.no_args arith_split_add, Attrib.no_args Attrib.undef_local_attribute),