src/HOL/ex/Quickcheck.thy

               val c = (fst o dest_Const o fst o strip_comb o fst
                 o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm;
             in
               lthy
               |> LocalTheory.theory (Code.del_eqns c
-                   #> PureThy.add_thm ((fst (dest_Free random') ^ "_code", thm), [Thm.kind_internal])
+                   #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal])
                    #-> Code.add_eqn)
             end;
         in
           thy
           |> TheoryTarget.instantiation ([tyco], vs, @{sort random})