src/HOL/Decision_Procs/ferrack_tac.ML

--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -73,7 +73,7 @@
 
 
 fun linr_tac ctxt q =
-    ObjectLogic.atomize_prems_tac
+    Object_Logic.atomize_prems_tac
         THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let