# HG changeset patch
# User berghofe
# Date 1186409281 -7200
# Node ID 409cd6eaa7eae5e37c68c3810c9dfa3c75aafe8a
# Parent  99e4722eceb150dd376b50e2620760ccc7be61c5
Added renaming function to prevent correctness proof for realizer
of induction rule to fail because of name clashes between parameters
and predicate variables.

diff -r 99e4722eceb1 -r 409cd6eaa7ea src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Mon Aug 06 16:05:25 2007 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon Aug 06 16:08:01 2007 +0200
@@ -271,6 +271,8 @@
       (foldr forall_intr_prf (prf_of rrule) (vs2 @ rs))))
   end;
 
+fun rename tab = map (fn x => the_default x (AList.lookup op = tab x));
+
 fun add_ind_realizer rsets intrs induct raw_induct elims (thy, vs) =
   let
     val qualifier = NameSpace.qualifier (name_of_thm induct);
@@ -365,9 +367,12 @@
 
     fun add_ind_realizer (thy, Ps) =
       let
+        val vs' = rename (map (pairself (fst o fst o dest_Var))
+          (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
+            (hd (prems_of (hd inducts))))), nparms))) vs;
         val rs = indrule_realizer thy induct raw_induct rsets params'
-          (vs @ Ps) rec_names rss' intrs dummies;
-        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs @ Ps) r
+          (vs' @ Ps) rec_names rss' intrs dummies;
+        val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
           (prop_of ind)) (rs ~~ inducts);
         val used = foldr add_term_free_names [] rlzs;
         val rnames = Name.variant_list used (replicate (length inducts) "r");
@@ -391,22 +396,22 @@
              [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm ((space_implode "_"
-          (NameSpace.qualified qualifier "induct" :: vs @ Ps @
+          (NameSpace.qualified qualifier "induct" :: vs' @ Ps @
              ["correctness"]), thm), []) thy;
         val thms = map (fn th => zero_var_indexes (rotate_prems ~1 (th RS mp)))
           (DatatypeAux.split_conj_thm thm');
         val ([thms'], thy'') = PureThy.add_thmss
           [((space_implode "_"
-             (NameSpace.qualified qualifier "inducts" :: vs @ Ps @
+             (NameSpace.qualified qualifier "inducts" :: vs' @ Ps @
                ["correctness"]), thms), [])] thy';
         val realizers = inducts ~~ thms' ~~ rlzs ~~ rs;
       in
         Extraction.add_realizers_i
           (map (fn (((ind, corr), rlz), r) =>
-              mk_realizer thy' (vs @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
+              mk_realizer thy' (vs' @ Ps) (Thm.get_name ind, ind, corr, rlz, r))
             realizers @ (case realizers of
              [(((ind, corr), rlz), r)] =>
-               [mk_realizer thy' (vs @ Ps) (NameSpace.qualified qualifier "induct",
+               [mk_realizer thy' (vs' @ Ps) (NameSpace.qualified qualifier "induct",
                   ind, corr, rlz, r)]
            | _ => [])) thy''
       end;