# HG changeset patch
# User oheimb
# Date 833566482 -7200
# Node ID e6656a445a33ef8f76b1b3249b5f4fdc0994e770
# Parent  1155c06fa9567c20cd9facabaaf401e161b21578
adapted proof of flat_codom

diff -r 1155c06fa956 -r e6656a445a33 src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri May 31 19:55:19 1996 +0200
+++ b/src/HOLCF/Fix.ML	Fri May 31 20:14:42 1996 +0200
@@ -726,14 +726,14 @@
         (res_inst_tac [("a","f`(UU::'a)")] (refl RS box_equals) 1),
         (etac allE 1),(etac allE 1),
         (dtac mp 1),
-        (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+        (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
         (etac disjE 1),
         (contr_tac 1),
         (atac 1),
         (etac allE 1),
         (etac allE 1),
         (dtac mp 1),
-        (res_inst_tac [("fo5","f")] (minimal RS monofun_cfun_arg) 1),
+        (res_inst_tac [("fo","f")] (minimal RS monofun_cfun_arg) 1),
         (etac disjE 1),
         (contr_tac 1),
         (atac 1)