src/HOL/Code_Evaluation.thy
changeset 38348 cf7b2121ad9d
parent 36176 3fe7e97ccca8
child 38857 97775f3e8722
--- a/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:40 2010 +0200
+++ b/src/HOL/Code_Evaluation.thy	Wed Aug 11 14:31:43 2010 +0200
@@ -64,7 +64,7 @@
         o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     in
       thy
-      |> Theory_Target.instantiation ([tyco], vs, @{sort term_of})
+      |> Class.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
       |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
       |> snd