use Library.Some/None instead of just Some/None in generated quickcheck code
authorkleing
Mon, 14 Jul 2003 14:44:06 +0200
changeset 14110 c45c94fa16f4
parent 14109 7aa5b79daffb
child 14111 993471c762b8
use Library.Some/None instead of just Some/None in generated quickcheck code
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,