src/HOL/Typerep.thy
changeset 33553 35f2b30593a8
parent 33384 1b5ba4e6a953
child 35115 446c5063e4fd
     1.1 --- a/src/HOL/Typerep.thy	Tue Nov 10 15:33:35 2009 +0100
     1.2 +++ b/src/HOL/Typerep.thy	Tue Nov 10 16:04:57 2009 +0100
     1.3 @@ -50,7 +50,7 @@
     1.4      val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     1.5    in
     1.6      thy
     1.7 -    |> TheoryTarget.instantiation ([tyco], vs, @{sort typerep})
     1.8 +    |> Theory_Target.instantiation ([tyco], vs, @{sort typerep})
     1.9      |> `(fn lthy => Syntax.check_term lthy eq)
    1.10      |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
    1.11      |> snd