# HG changeset patch
# User wenzelm
# Date 1214227613 -7200
# Node ID 385c0ce331737ad568cda34e5f1d2797230321bb
# Parent  a12978a1126a469c0ea43e9cb45f4771ce4df4d1
tuned get_inductT: *all* rules for missing instantiation;
exported get_inductT;

diff -r a12978a1126a -r 385c0ce33173 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Mon Jun 23 15:26:52 2008 +0200
+++ b/src/Tools/induct.ML	Mon Jun 23 15:26:53 2008 +0200
@@ -62,6 +62,7 @@
   val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
   val cases_tac: Proof.context -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
+  val get_inductT: Proof.context -> term option list list -> thm list list
   val induct_tac: Proof.context -> (string option * term) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic
@@ -567,18 +568,16 @@
     ...   induct ... r   - explicit rule
 *)
 
-local
-
 fun get_inductT ctxt insts =
-  fold_rev multiply (insts |> map_filter (fn [] => NONE | ts => List.last ts)
-    |> map (find_inductT ctxt o Term.fastype_of)) [[]]
+  fold_rev multiply (insts |> map
+      ((fn [] => NONE | ts => List.last ts) #>
+        (fn NONE => TVar (("'a", 0), []) | SOME t => Term.fastype_of t) #>
+        find_inductT ctxt)) [[]]
   |> filter_out (forall PureThy.is_internal);
 
 fun get_inductP ctxt (fact :: _) = map single (find_inductP ctxt (Thm.concl_of fact))
   | get_inductP _ _ = [];
 
-in
-
 fun induct_tac ctxt def_insts arbitrary taking opt_rule facts =
   let
     val thy = ProofContext.theory_of ctxt;
@@ -629,8 +628,6 @@
     THEN_ALL_NEW_CASES rulify_tac
   end;
 
-end;
-
 
 
 (** coinduct method **)