--- 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;