src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Thu Jun 09 22:25:25 2011 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Jun 09 23:12:02 2011 +0200
@@ -63,9 +63,9 @@
   let
     val cn = cterm_of thy (Var (("n", 0), HOLogic.natT))
     and ct = cterm_of thy t
-  in instantiate ([], [(cn, ct)]) @{thm le0} end;
+  in Drule.instantiate_normalize ([], [(cn, ct)]) @{thm le0} end;
 
-end;  (* LA_Logic *)
+end;
 
 
 (* arith context data *)