# HG changeset patch
# User wenzelm
# Date 1277381948 -7200
# Node ID d9c2fdd6614f3d99bda0c46b412542559e2c4875
# Parent  f4016fca4ff9874afdd6123eb113c98158447182
avoid equality on abstract type Pretty.T;

diff -r f4016fca4ff9 -r d9c2fdd6614f src/HOL/Tools/inductive_codegen.ML
--- 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 ")"])))