src/HOL/Library/Eval.thy

       val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     in
       thy
       |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
       |> `(fn lthy => Syntax.check_term lthy eq)
-      |-> (fn eq => Specification.definition (NONE, (("", []), eq)))
+      |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
       |> snd
       |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
       |> LocalTheory.exit
       |> ProofContext.theory_of
     end;