Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
avoid equality on abstract type Pretty.T;
authorwenzelm
Thu, 24 Jun 2010 14:19:08 +0200
changeset 37527 d9c2fdd6614f
parent 37526 f4016fca4ff9
child 37528 42804fb5dd92
avoid equality on abstract type Pretty.T;
src/HOL/Tools/inductive_codegen.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/inductive_codegen.ML	Thu Jun 24 13:31:26 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Thu Jun 24 14:19:08 2010 +0200
@@ -334,10 +334,10 @@
   in
     Pretty.block
      ([str "(fn ", mk_tuple out_ps, str " =>", Pretty.brk 1] @
-      (Pretty.block ((if eqs=[] then [] else str "if " ::
+      (Pretty.block ((if null eqs then [] else str "if " ::
          [Pretty.block eqs, Pretty.brk 1, str "then "]) @
          (success_p ::
-          (if eqs=[] then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
+          (if null eqs then [] else [Pretty.brk 1, str "else DSeq.empty"]))) ::
        (if can_fail then
           [Pretty.brk 1, str "| _ => DSeq.empty)"]
         else [str ")"])))
isabelle