src/HOL/Code_Evaluation.thy
changeset 33553 35f2b30593a8
parent 33473 3b275a0bf18c
child 33632 6ea8a4cce9e7
     1.1 --- a/src/HOL/Code_Evaluation.thy	Tue Nov 10 15:33:35 2009 +0100
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Tue Nov 10 16:04:57 2009 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4          o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     1.5      in
     1.6        thy
     1.7 -      |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
     1.8 +      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
     1.9        |> `(fn lthy => Syntax.check_term lthy eq)
    1.10        |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    1.11        |> snd