diff -r 231e261fd6bc -r ddfd021884b4 src/HOL/Tools/code_evaluation.ML
--- a/src/HOL/Tools/code_evaluation.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/code_evaluation.ML	Sun May 29 15:40:25 2016 +0200
@@ -43,7 +43,7 @@
     thy
     |> 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))
+    |-> (fn eq => Specification.definition NONE [] [] ((Binding.name (triv_name_of eq), []), eq))
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
   end;