diff -r 69394731c419 -r fcbd7f0c52c3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/overloading.ML	Mon Jun 01 18:59:20 2015 +0200
@@ -161,7 +161,7 @@
       if mx <> NoSyn
       then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
       else lthy |> define_overloaded (c, U) (v, checked) (b_def, rhs)
-  | NONE => lthy |> Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) params);
+  | NONE => lthy |> Generic_Target.theory_target_foundation (((b, U), mx), (b_def, rhs)) params);
 
 fun pretty lthy =
   let
@@ -201,8 +201,8 @@
     |> synchronize_syntax
     |> Local_Theory.init (Sign.naming_of thy)
        {define = Generic_Target.define foundation,
-        notes = Generic_Target.notes Generic_Target.theory_notes,
-        abbrev = Generic_Target.abbrev Generic_Target.theory_abbrev,
+        notes = Generic_Target.notes Generic_Target.theory_target_notes,
+        abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
         subscription = Generic_Target.theory_registration,
         pretty = pretty,