diff -r 55827fc7c0dd -r 41c6b99c5fb7 src/HOL/Tools/lin_arith.ML
--- 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))
     ]