# HG changeset patch
# User haftmann
# Date 1232736709 -3600
# Node ID 1219985d24b528650dad80fb672b136da76aa606
# Parent  2eeb09477ed3d6a9e3c3b3a02df14e8f07723492
avoiding misleading name duplicate

diff -r 2eeb09477ed3 -r 1219985d24b5 src/HOL/Tools/datatype_case.ML
--- a/src/HOL/Tools/datatype_case.ML	Fri Jan 23 19:51:48 2009 +0100
+++ b/src/HOL/Tools/datatype_case.ML	Fri Jan 23 19:51:49 2009 +0100
@@ -419,21 +419,21 @@
 
 (* destruct nested patterns *)
 
-fun strip_case' dest (pat, rhs) =
+fun strip_case'' dest (pat, rhs) =
   case dest (Term.add_free_names pat []) rhs of
     SOME (exp as Free _, clauses) =>
       if member op aconv (OldTerm.term_frees pat) exp andalso
         not (exists (fn (_, rhs') =>
           member op aconv (OldTerm.term_frees rhs') exp) clauses)
       then
-        maps (strip_case' dest) (map (fn (pat', rhs') =>
+        maps (strip_case'' dest) (map (fn (pat', rhs') =>
           (subst_free [(exp, pat')] pat, rhs')) clauses)
       else [(pat, rhs)]
   | _ => [(pat, rhs)];
 
 fun gen_strip_case dest t = case dest [] t of
     SOME (x, clauses) =>
-      SOME (x, maps (strip_case' dest) clauses)
+      SOME (x, maps (strip_case'' dest) clauses)
   | NONE => NONE;
 
 val strip_case = gen_strip_case oo dest_case;