# HG changeset patch
# User haftmann
# Date 1260784864 -3600
# Node ID ff8b2ac0134c30954117678ce0b79164fb793ed4
# Parent  652719832159057a9d973f7c07def35bef111632# Parent  420234017d39640da983f0e66055373b1ebd48db
merged

diff -r 652719832159 -r ff8b2ac0134c src/Tools/Code/code_haskell.ML
--- a/src/Tools/Code/code_haskell.ML	Mon Dec 14 10:59:46 2009 +0100
+++ b/src/Tools/Code/code_haskell.ML	Mon Dec 14 11:01:04 2009 +0100
@@ -330,11 +330,12 @@
     fun deriving_show tyco =
       let
         fun deriv _ "fun" = false
-          | deriv tycos tyco = member (op =) tycos tyco orelse
-              case try (Graph.get_node program) tyco
+          | deriv tycos tyco = not (tyco = Code_Thingol.fun_tyco)
+              andalso (member (op =) tycos tyco
+              orelse case try (Graph.get_node program) tyco
                 of SOME (Code_Thingol.Datatype (_, (_, cs))) => forall (deriv' (tyco :: tycos))
                     (maps snd cs)
-                 | NONE => true
+                 | NONE => true)
         and deriv' tycos (tyco `%% tys) = deriv tycos tyco
               andalso forall (deriv' tycos) tys
           | deriv' _ (ITyVar _) = true
diff -r 652719832159 -r ff8b2ac0134c src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Dec 14 10:59:46 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Dec 14 11:01:04 2009 +0100
@@ -36,6 +36,7 @@
 signature CODE_THINGOL =
 sig
   include BASIC_CODE_THINGOL
+  val fun_tyco: string
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
@@ -388,8 +389,10 @@
    of SOME const' => (const', naming)
     | NONE => declare_const thy const naming;
 
+val fun_tyco = "Pure.fun.tyco" (*depends on suffix_tyco and namify_tyco!*);
+
 val unfold_fun = unfoldr
-  (fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
+  (fn tyco `%% [ty1, ty2] => if tyco = fun_tyco then SOME (ty1, ty2) else NONE
     | _ => NONE); (*depends on suffix_tyco and namify_tyco!*)
 
 end; (* local *)