changeset 33553 | 35f2b30593a8 |
parent 33522 | 737589bb9bb8 |
child 35743 | c506c029a082 |
--- a/src/HOL/Tools/typecopy.ML Tue Nov 10 15:33:35 2009 +0100 +++ b/src/HOL/Tools/typecopy.ML Tue Nov 10 16:04:57 2009 +0100 @@ -113,7 +113,7 @@ thy |> Code.add_datatype [constr] |> Code.add_eqn proj_eq - |> TheoryTarget.instantiation ([tyco], vs, [HOLogic.class_eq]) + |> Theory_Target.instantiation ([tyco], vs, [HOLogic.class_eq]) |> `(fn lthy => Syntax.check_term lthy eq) |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))