Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Quickcheck/random_generators.ML
changeset 63239 d562c9948dee
parent 63180 ddfd021884b4
child 63352 4eaf35781b23 
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Mon Jun 06 21:28:46 2016 +0200
@@ -179,7 +179,7 @@
     |> random_aux_primrec_multi (name ^ prfx) proto_eqs
     |-> prove_simps
     |-> (fn simps => Local_Theory.note
-      ((b, Code.add_default_eqn_attrib :: @{attributes [simp, nitpick_simp]}), simps))
+      ((b, Code.add_default_eqn_attrib Code.Equation:: @{attributes [simp, nitpick_simp]}), simps))
     |> snd
   end
isabelle