replaced constant 0 by HOL.zero
authorhaftmann
Wed, 27 Sep 2006 16:33:08 +0200
changeset 20731 2ef8b7332b4f
parent 20730 da903f59e9ba
child 20732 275f9bd2ead9
replaced constant 0 by HOL.zero
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;