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 63180 ddfd021884b4
parent 63064 2f18172214c8
child 63239 d562c9948dee 
--- a/src/HOL/Tools/Quickcheck/random_generators.ML	Sat May 28 23:55:41 2016 +0200
+++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Sun May 29 15:40:25 2016 +0200
@@ -266,7 +266,7 @@
     |> random_aux_specification prfx random_auxN auxs_eqs
     |> `(fn lthy => map (Syntax.check_term lthy) random_defs)
     |-> (fn random_defs' => fold_map (fn random_def =>
-          Specification.definition NONE []
+          Specification.definition NONE [] []
             ((Binding.concealed Binding.empty, []), random_def)) random_defs')
     |> snd
     |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt [])
isabelle