# HG changeset patch
# User wenzelm
# Date 1213119272 -7200
# Node ID 7d643d3935b1c8857b55f9af1651b1f327421295
# Parent  9cc5964f7f3c82ce1989e334b0f2df2bce8d5702
case_tac: accomodate change in bound variable name;

diff -r 9cc5964f7f3c -r 7d643d3935b1 src/HOL/Word/WordShift.thy
--- a/src/HOL/Word/WordShift.thy	Tue Jun 10 19:15:23 2008 +0200
+++ b/src/HOL/Word/WordShift.thy	Tue Jun 10 19:34:32 2008 +0200
@@ -121,12 +121,12 @@
        apply arith
       apply arith
      apply (erule thin_rl)
-     apply (case_tac n)
+     apply (case_tac nat)
       apply safe
       apply simp
      apply simp
     apply (erule thin_rl)
-    apply (case_tac n)
+    apply (case_tac nat)
      apply safe
      apply simp
     apply simp