# HG changeset patch
# User blanchet
# Date 1398291818 -7200
# Node ID 5545bfdfefcc11740c846dd30be1a7d7e5a0fa44
# Parent  71a8ac5d039f5271e4c89c472b5a41486312a037
avoid name shadowing

diff -r 71a8ac5d039f -r 5545bfdfefcc src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Apr 24 00:08:48 2014 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Thu Apr 24 00:23:38 2014 +0200
@@ -174,16 +174,16 @@
 
 subsection {* Alternative rules for @{text length} *}
 
-definition size_list :: "'a list => nat"
-where "size_list = size"
+definition size_list' :: "'a list => nat"
+where "size_list' = size"
 
-lemma size_list_simps:
-  "size_list [] = 0"
-  "size_list (x # xs) = Suc (size_list xs)"
-by (auto simp add: size_list_def)
+lemma size_list'_simps:
+  "size_list' [] = 0"
+  "size_list' (x # xs) = Suc (size_list' xs)"
+by (auto simp add: size_list'_def)
 
-declare size_list_simps[code_pred_def]
-declare size_list_def[symmetric, code_pred_inline]
+declare size_list'_simps[code_pred_def]
+declare size_list'_def[symmetric, code_pred_inline]
 
 
 subsection {* Alternative rules for @{text list_all2} *}
diff -r 71a8ac5d039f -r 5545bfdfefcc src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 24 00:08:48 2014 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Thu Apr 24 00:23:38 2014 +0200
@@ -1077,12 +1077,12 @@
 *)
 subsection {* Inverting list functions *}
 
-code_pred [inductify, skip_proof] size_list .
-code_pred [new_random_dseq inductify] size_list .
-thm size_listP.equation
-thm size_listP.new_random_dseq_equation
+code_pred [inductify, skip_proof] size_list' .
+code_pred [new_random_dseq inductify] size_list' .
+thm size_list'P.equation
+thm size_list'P.new_random_dseq_equation
 
-values [new_random_dseq 2,3,10] 3 "{xs. size_listP (xs::nat list) (5::nat)}"
+values [new_random_dseq 2,3,10] 3 "{xs. size_list'P (xs::nat list) (5::nat)}"
 
 code_pred (expected_modes: i => o => bool, o => i => bool, i => i => bool) [inductify, skip_proof] List.concat .
 thm concatP.equation