# HG changeset patch
# User berghofe
# Date 1085168915 -7200
# Node ID 50581f2b2c0ef74ca87d130b8582f7a3e73fabcc
# Parent  a405aadff16c360059cefaa18f0a59a9244b82df
Adapted to new syntax for case expressions.

diff -r a405aadff16c -r 50581f2b2c0e src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Fri May 21 21:48:03 2004 +0200
+++ b/src/HOL/Numeral.thy	Fri May 21 21:48:35 2004 +0200
@@ -109,8 +109,8 @@
   bin_add_Min: "bin_add bin.Min w = bin_pred w"
   bin_add_BIT:
     "bin_add (v BIT x) w =
-       (case w of Pls => v BIT x
-                | Min => bin_pred (v BIT x)
+       (case w of bin.Pls => v BIT x
+                | bin.Min => bin_pred (v BIT x)
                 | (w BIT y) =>
       	            NCons (bin_add v (if (x & y) then bin_succ w else w))
 	                  (x~=y))"