--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Mon Jul 03 14:25:07 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Jul 02 20:13:38 2017 +0200
@@ -382,11 +382,11 @@
val eqs = map (fn eq => Goal.prove lthy argnames [] eq
(fn {context = ctxt, ...} => ALLGOALS (Skip_Proof.cheat_tac ctxt))) eqs_t
in
- fold (fn (name, eq) => Local_Theory.note
- ((Binding.qualify true prfx
- (Binding.qualify true name (Binding.name "simps")),
- [Code.add_default_eqn_attrib Code.Equation]), [eq]) #> snd)
- (names ~~ eqs) lthy
+ lthy
+ |> fold_map (fn (name, eq) => Local_Theory.note
+ (((Binding.qualify true prfx o Binding.qualify true name) (Binding.name "simps"), []), [eq]))
+ (names ~~ eqs)
+ |-> (fn notes => Code.declare_default_eqns (map (rpair true) (maps snd notes)))
end)