--- a/src/HOL/Code_Eval.thy Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Code_Eval.thy Thu Dec 04 14:43:33 2008 +0100
@@ -63,7 +63,7 @@
thy
|> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
|> `(fn lthy => Syntax.check_term lthy eq)
- |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
+ |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
|> snd
|> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
|> LocalTheory.exit_global