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/Pure/codegen.ML
changeset 14110 c45c94fa16f4
parent 14105 85d1a908f024
child 14135 f8a25218b423 
--- 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,
isabelle