src/HOL/Tools/Quickcheck/narrowing_generators.ML

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Sun Jul 02 20:13:38 2017 +0200
@@ -110,8 +110,7 @@
     val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs
   in
     thy
-    |> Code.del_eqns const
-    |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*)
+    |> Code.declare_default_eqns_global (map (rpair true) eqs)
   end
 
 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =