src/HOL/Library/RType.thy

     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
     |> TheoryTarget.instantiation ([tyco], vs, @{sort rtype})
     |> `(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;