1.1 --- a/src/HOL/NSA/transfer.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/NSA/transfer.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -63,7 +63,7 @@
     1.4      val u = unstar_term consts t'
     1.5      val tac =
     1.6        rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
     1.7 -      ALLGOALS ObjectLogic.full_atomize_tac THEN
     1.8 +      ALLGOALS Object_Logic.full_atomize_tac THEN
     1.9        match_tac [transitive_thm] 1 THEN
    1.10        resolve_tac [@{thm transfer_start}] 1 THEN
    1.11        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN