src/HOL/Tools/lin_arith.ML

--- a/src/HOL/Tools/lin_arith.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -901,7 +901,7 @@
 in
 
 fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+  Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
 
 val tac = gen_tac true;