changeset 38348 | cf7b2121ad9d |
parent 37469 | 1436d6f28f17 |
child 38528 | bbaaaf6f1cbe |
--- a/src/HOL/Tools/typecopy.ML Wed Aug 11 14:31:40 2010 +0200 +++ b/src/HOL/Tools/typecopy.ML Wed Aug 11 14:31:43 2010 +0200 @@ -116,7 +116,7 @@ thy |> Code.add_datatype [constr] |> Code.add_eqn proj_constr - |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq]) + |> Class.instantiation ([tyco], vs, [HOLogic.class_eq]) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))