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/ex/Quickcheck.thy
changeset 28084 a05ca48ef263
parent 28083 103d9282a946
child 28145 af3923ed4786 
--- a/src/HOL/ex/Quickcheck.thy	Tue Sep 02 14:10:45 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy	Tue Sep 02 16:55:33 2008 +0200
@@ -132,7 +132,7 @@
                  (map (fn eq => ((Name.no_binding, [del_func]), eq)) eqs')
           |-> add_code
           |> `(fn lthy => Syntax.check_term lthy eq)
-          |-> (fn eq => Specification.definition (NONE, ((Name.no_binding, []), eq)))
+          |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
           |> snd
           |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
           |> LocalTheory.exit
@@ -261,7 +261,7 @@
   in
     thy
     |> TheoryTarget.init NONE
-    |> Specification.definition (NONE, ((Name.no_binding, []), eq))
+    |> Specification.definition (NONE, (Attrib.no_binding, eq))
     |> snd
     |> LocalTheory.exit
     |> ProofContext.theory_of
isabelle