--- a/src/HOL/Tools/lin_arith.ML Fri Mar 07 22:19:52 2014 +0100
+++ b/src/HOL/Tools/lin_arith.ML Fri Mar 07 22:30:58 2014 +0100
@@ -33,7 +33,7 @@
structure LA_Logic: LIN_ARITH_LOGIC =
struct
-val ccontr = ccontr;
+val ccontr = @{thm ccontr};
val conjI = conjI;
val notI = notI;
val sym = sym;
@@ -733,7 +733,7 @@
EVERY' [
REPEAT_DETERM o etac rev_mp,
cond_split_tac,
- rtac ccontr,
+ rtac @{thm ccontr},
prem_nnf_tac ctxt,
TRY o REPEAT_ALL_NEW (DETERM o (eresolve_tac [conjE, exE] ORELSE' etac disjE))
]