# HG changeset patch
# User berghofe
# Date 1197912644 -3600
# Node ID f3815084e89ebf7e86283f35232a7f11d1d1bcac
# Parent  2488fc510178b73c8b887b89b27cd2a8698229ae
- Removed redundant head_len field in datatype_info
- Added new alt_names field in datatype_info
- indtac now takes additional list of variables as argument

diff -r 2488fc510178 -r f3815084e89e src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Dec 17 18:27:48 2007 +0100
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Dec 17 18:30:44 2007 +0100
@@ -27,7 +27,7 @@
   val app_bnds : term -> int -> term
 
   val cong_tac : int -> tactic
-  val indtac : thm -> int -> tactic
+  val indtac : thm -> string list -> int -> tactic
   val exh_tac : (string -> thm) -> int -> tactic
 
   datatype simproc_dist = QuickAndDirty
@@ -123,21 +123,25 @@
 
 (* instantiate induction rule *)
 
-fun indtac indrule i st =
+fun indtac indrule indnames i st =
   let
     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
       (Logic.strip_imp_concl (List.nth (prems_of st, i - 1))));
     val getP = if can HOLogic.dest_imp (hd ts) then
       (apfst SOME) o HOLogic.dest_imp else pair NONE;
+    val flt = if null indnames then I else
+      filter (fn Free (s, _) => s mem indnames | _ => false);
     fun abstr (t1, t2) = (case t1 of
-        NONE => let val [Free (s, T)] = add_term_frees (t2, [])
-          in absfree (s, T, t2) end
-      | SOME (_ $ t') => Abs ("x", fastype_of t', abstract_over (t', t2)))
+        NONE => (case flt (term_frees t2) of
+            [Free (s, T)] => SOME (absfree (s, T, t2))
+          | _ => NONE)
+      | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
     val cert = cterm_of (Thm.theory_of_thm st);
-    val Ps = map (cert o head_of o snd o getP) ts;
-    val indrule' = cterm_instantiate (Ps ~~
-      (map (cert o abstr o getP) ts')) indrule
+    val insts = List.mapPartial (fn (t, u) => case abstr (getP u) of
+        NONE => NONE
+      | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
+    val indrule' = cterm_instantiate insts indrule
   in
     rtac indrule' i st
   end;
@@ -179,7 +183,7 @@
 
 type datatype_info =
   {index : int,
-   head_len : int,
+   alt_names : string list option,
    descr : descr,
    sorts : (string * sort) list,
    rec_names : string list,