--- a/src/Pure/Isar/class.ML Mon Jun 01 18:59:20 2015 +0200
+++ b/src/Pure/Isar/class.ML Mon Jun 01 18:59:20 2015 +0200
@@ -580,7 +580,7 @@
SOME c =>
if mx <> NoSyn then error ("Illegal mixfix syntax for overloaded constant " ^ quote c)
else lthy |> define_overloaded (c, U) (Binding.name_of b) (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
@@ -645,8 +645,8 @@
|> synchronize_inst_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,