# HG changeset patch
# User huffman
# Date 1346947190 25200
# Node ID 6096da55d2d6d881053cf637a5ea28a0d2b0b98f
# Parent  4b5fa9d5e3305d8af85fb2d3990f81875671fb08
countable_datatype method: pre-instantiate induction rule to avoid failure with e.g. datatype a = A "b list" and b = B "a"

diff -r 4b5fa9d5e330 -r 6096da55d2d6 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Thu Sep 06 17:12:24 2012 +0200
+++ b/src/HOL/Library/Countable.thy	Thu Sep 06 08:59:50 2012 -0700
@@ -288,12 +288,17 @@
         val induct_thms = #inducts (snd induct_info)
         val alist = pred_names ~~ induct_thms
         val induct_thm = the (AList.lookup (op =) alist pred_name)
+        val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
+        val thy = Proof_Context.theory_of ctxt
+        val insts = vars |> map (fn (_, T) => try (Thm.cterm_of thy)
+          (Const (@{const_name Countable.finite_item}, T)))
+        val induct_thm' = Drule.instantiate' [] insts induct_thm
         val rules = @{thms finite_item.intros}
       in
         SOLVED' (fn i => EVERY
           [rtac @{thm countable_datatype} i,
            rtac typedef_thm i,
-           etac induct_thm i,
+           etac induct_thm' i,
            REPEAT (resolve_tac rules i ORELSE atac i)]) 1
       end)
 *}