1.1 --- a/src/HOL/Tools/typedef.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/typedef.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -130,7 +130,7 @@
     1.4            in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
     1.5  
     1.6      fun typedef_result inhabited =
     1.7 -      ObjectLogic.typedecl (tname, vs, mx)
     1.8 +      Object_Logic.typedecl (tname, vs, mx)
     1.9        #> snd
    1.10        #> Sign.add_consts_i
    1.11          [(Rep_name, newT --> oldT, NoSyn),