# HG changeset patch
# User haftmann
# Date 1159367588 -7200
# Node ID 2ef8b7332b4f00963cbd929109a4862847a2214c
# Parent  da903f59e9ba439bbea7decd61e705dd6f549ff0
replaced constant 0 by HOL.zero

diff -r da903f59e9ba -r 2ef8b7332b4f src/HOLCF/domain/theorems.ML
--- a/src/HOLCF/domain/theorems.ML	Wed Sep 27 07:09:19 2006 +0200
+++ b/src/HOLCF/domain/theorems.ML	Wed Sep 27 16:33:08 2006 +0200
@@ -645,7 +645,7 @@
   val take_stricts' = rewrite_rule copy_take_defs take_stricts;
   fun take_0 n dn =
     let
-      val goal = mk_trp ((dc_take dn $ %%:"0") `% x_name n === UU);
+      val goal = mk_trp ((dc_take dn $ %%:"HOL.zero") `% x_name n === UU);
     in pg axs_take_def goal [simp_tac iterate_Cprod_ss 1] end;
   val take_0s = mapn take_0 1 dnames;
   val c_UU_tac = case_UU_tac (take_stricts'::copy_con_rews) 1;