diff -r 19000bb11ff5 -r cf7b2121ad9d src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed Aug 11 14:31:43 2010 +0200
@@ -47,6 +47,8 @@
   val read_multi_arity: theory -> xstring list * xstring list * xstring
     -> string list * (string * sort) list * sort
   val type_name: string -> string
+  val instantiation: string list * (string * sort) list * sort -> theory -> local_theory
+  val instantiation_cmd: xstring list * xstring list * xstring -> theory -> local_theory
 
   (*subclasses*)
   val register_subclass: class * class -> morphism option -> Element.witness option
@@ -580,6 +582,35 @@
       (Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params)
   end;
 
+fun syntax_error c = error ("Illegal mixfix syntax for overloaded constant " ^ quote c);
+
+fun instantiation_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy =
+  case instantiation_param lthy b
+   of SOME c => if mx <> NoSyn then syntax_error c
+        else lthy |> Local_Theory.theory_result (AxClass.declare_overloaded (c, U)
+            ##>> AxClass.define_overloaded b_def (c, rhs))
+          ||> confirm_declaration b
+    | NONE => lthy |>
+        Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params);
+
+fun instantiation arities thy =
+  thy
+  |> init_instantiation arities
+  |> Local_Theory.init NONE ""
+     {define = Generic_Target.define instantiation_foundation,
+      notes = Generic_Target.notes
+        (fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts),
+      abbrev = Generic_Target.abbrev
+        (fn prmode => fn (b, mx) => fn (t, _) => fn _ => Generic_Target.theory_abbrev prmode ((b, mx), t)),
+      declaration = K Generic_Target.theory_declaration,
+      syntax_declaration = K Generic_Target.theory_declaration,
+      pretty = single o pretty_instantiation,
+      reinit = instantiation arities o ProofContext.theory_of,
+      exit = Local_Theory.target_of o conclude_instantiation};
+
+fun instantiation_cmd arities thy =
+  instantiation (read_multi_arity thy arities) thy;
+
 
 (* simplified instantiation interface with no class parameter *)