# HG changeset patch
# User berghofe
# Date 953159806 -3600
# Node ID 17231d71171a1d853569c8c603cb3fed37ba2512
# Parent  07d3e6383822b62e0b84022f0624aed9a4649440
- Fixed bug in prove_casedist_thms (proof failed because of
  name clashes)
- Now returns theorems with correct names in derivations

diff -r 07d3e6383822 -r 17231d71171a src/HOL/Tools/datatype_abs_proofs.ML
--- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 15 18:52:07 2000 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 15 23:36:46 2000 +0100
@@ -24,7 +24,7 @@
   val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
-        simpset -> thm -> theory -> theory * string list * thm list
+        simpset -> thm -> theory -> theory * (string list * thm list)
   val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
       string list -> thm list -> theory -> theory * (thm list list * string list)
@@ -62,13 +62,14 @@
     val recTs = get_rec_types descr' sorts;
     val newTs = take (length (hd descr), recTs);
 
+    val {maxidx, ...} = rep_thm induct;
     val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
 
     fun prove_casedist_thm ((i, t), T) =
       let
         val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
           Abs ("z", T', Const ("True", T''))) induct_Ps;
-        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", 0), T), Bound 0) $
+        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
           Var (("P", 0), HOLogic.boolT))
         val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
         val cert = cterm_of (Theory.sign_of thy);
@@ -280,12 +281,12 @@
            (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
 
   in
-    (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
-             (#1 o PureThy.add_thmss [(("recs", rec_thms), [])]) |>
-             Theory.parent_path,
-     reccomb_names, rec_thms)
+    thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
+    PureThy.add_thmss [(("recs", rec_thms), [])] |>>
+    Theory.parent_path |> apsnd (pair reccomb_names o flat)
   end;
 
+
 (***************************** case combinators *******************************)
 
 fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
@@ -349,13 +350,15 @@
     val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
       (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
         (fn _ => [rtac refl 1])))
-          (DatatypeProp.make_cases new_type_names descr sorts thy2);
+          (DatatypeProp.make_cases new_type_names descr sorts thy2)
 
-    val thy3 = thy2 |> Theory.add_trrules_i
+  in
+    thy2 |> Theory.add_trrules_i
       (DatatypeProp.make_case_trrules new_type_names descr) |>
-      parent_path flat_names;
-
-  in thy3 |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names) end;
+    parent_path flat_names |>
+    store_thmss "cases" new_type_names case_thms |>
+    apsnd (rpair case_names)
+  end;
 
 
 (******************************* case splitting *******************************)
@@ -453,12 +456,12 @@
         (DatatypeProp.make_size new_type_names descr sorts thy')
 
   in
-    (thy' |> Theory.add_path big_name |>
-             (#1 o PureThy.add_thmss [(("size", size_thms), [])]) |>
-             Theory.parent_path,
-     size_thms)
+    thy' |> Theory.add_path big_name |>
+    PureThy.add_thmss [(("size", size_thms), [])] |>>
+    Theory.parent_path |> apsnd flat
   end;
 
+
 (************************* additional theorems for TFL ************************)
 
 fun prove_nchotomys new_type_names descr sorts casedist_thms thy =