diff -r f6d9e0e0b153 -r 1de908189869 src/HOL/ex/Quickcheck.thy
--- a/src/HOL/ex/Quickcheck.thy	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/ex/Quickcheck.thy	Thu Dec 04 14:43:33 2008 +0100
@@ -151,11 +151,11 @@
           thy
           |> TheoryTarget.instantiation ([tyco], vs, @{sort random})
           |> PrimrecPackage.add_primrec
-               [(Name.binding (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
-                 (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
+               [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)]
+                 (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs')
           |-> add_code
           |> `(fn lthy => Syntax.check_term lthy eq)
-          |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
+          |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq)))
           |> snd
           |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
           |> LocalTheory.exit_global