# HG changeset patch
# User kleing
# Date 1058186646 -7200
# Node ID c45c94fa16f4d7355e77e8043c32860b0f004e54
# Parent  7aa5b79daffbd54d4f89d19d2f81323e09140dce
use Library.Some/None instead of just Some/None in generated quickcheck code

diff -r 7aa5b79daffb -r c45c94fa16f4 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Fri Jul 11 15:01:41 2003 +0200
+++ b/src/Pure/codegen.ML	Mon Jul 14 14:44:06 2003 +0200
@@ -568,9 +568,9 @@
             Pretty.brk 1, Pretty.str "in", Pretty.brk 1,
             Pretty.block [Pretty.str "if ",
               mk_app false (Pretty.str "testf") (map (Pretty.str o fst) frees),
-              Pretty.brk 1, Pretty.str "then None",
+              Pretty.brk 1, Pretty.str "then Library.None",
               Pretty.brk 1, Pretty.str "else ",
-              Pretty.block [Pretty.str "Some ", Pretty.block (Pretty.str "[" ::
+              Pretty.block [Pretty.str "Library.Some ", Pretty.block (Pretty.str "[" ::
                 flat (separate [Pretty.str ",", Pretty.brk 1]
                   (map (fn (s, T) => [Pretty.block
                     [Pretty.str ("(" ^ quote s ^ ","), Pretty.brk 1,