diff -r 46a0dc9b51bb -r 715163ec93c0 src/Tools/code/code_haskell.ML
--- a/src/Tools/code/code_haskell.ML	Thu Sep 25 09:28:07 2008 +0200
+++ b/src/Tools/code/code_haskell.ML	Thu Sep 25 09:28:08 2008 +0200
@@ -153,10 +153,11 @@
               )
             ]
           end
-      | pr_stmt (name, Code_Thingol.Fun ((vs, ty), eqs)) =
+      | pr_stmt (name, Code_Thingol.Fun ((vs, ty), raw_eqs)) =
           let
+            val eqs = filter (snd o snd) raw_eqs;
             val tyvars = intro_vars (map fst vs) init_syms;
-            fun pr_eq ((ts, t), thm) =
+            fun pr_eq ((ts, t), (thm, _)) =
               let
                 val consts = map_filter
                   (fn c => if (is_some o syntax_const) c
@@ -248,7 +249,7 @@
       | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
           let
             val tyvars = intro_vars (map fst vs) init_syms;
-            fun pr_instdef ((classparam, c_inst), thm) =
+            fun pr_instdef ((classparam, c_inst), (thm, _)) =
               semicolon [
                 (str o classparam_name class) classparam,
                 str "=",