# HG changeset patch
# User wenzelm
# Date 957566773 -7200
# Node ID a1297de19ec77ab1bcd96f4714af5d338e444a2d
# Parent  d04923e183c787a7cb922abee6c42057da2d81ca
fixed clash with new 'abs' const;

diff -r d04923e183c7 -r a1297de19ec7 src/HOLCF/Cfun3.ML
--- a/src/HOLCF/Cfun3.ML	Fri May 05 22:37:04 2000 +0200
+++ b/src/HOLCF/Cfun3.ML	Sat May 06 00:46:13 2000 +0200
@@ -410,13 +410,13 @@
 
 
 qed_goal "isorep_defined" thy 
-        "[|!x. rep`(abs`x)=x;!y. abs`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
+        "[|!x. rep`(ab`x)=x;!y. ab`(rep`y)=y; z~=UU|] ==> rep`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (etac swap 1),
         (dtac notnotD 1),
-        (dres_inst_tac [("f","abs")] cfun_arg_cong 1),
+        (dres_inst_tac [("f","ab")] cfun_arg_cong 1),
         (etac box_equals 1),
         (fast_tac HOL_cs 1),
         (etac (iso_strict RS conjunct1) 1),
@@ -424,7 +424,7 @@
         ]);
 
 qed_goal "isoabs_defined" thy 
-        "[|!x. rep`(abs`x) = x;!y. abs`(rep`y)=y ; z~=UU|] ==> abs`z ~= UU"
+        "[|!x. rep`(ab`x) = x;!y. ab`(rep`y)=y ; z~=UU|] ==> ab`z ~= UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),