--- a/src/HOL/Tools/lin_arith.ML Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri Sep 18 09:07:50 2009 +0200
@@ -51,7 +51,7 @@
atomize (thm RS conjunct1) @ atomize (thm RS conjunct2)
| _ => [thm];
-fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name "Not"}, _) $ t)) = TP $ t
+fun neg_prop ((TP as Const("Trueprop", _)) $ (Const (@{const_name Not}, _) $ t)) = TP $ t
| neg_prop ((TP as Const("Trueprop", _)) $ t) = TP $ (HOLogic.Not $t)
| neg_prop t = raise TERM ("neg_prop", [t]);