1.1 --- a/src/HOL/Library/Countable.thy	Mon Jul 05 15:12:20 2010 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Mon Jul 05 15:12:20 2010 +0200
     1.3 @@ -110,26 +110,20 @@
     1.4    "to_nat_typerep (Typerep.Typerep c ts) = to_nat (to_nat c, to_nat (map to_nat_typerep ts))"
     1.5  
     1.6  instance proof (rule countable_classI)
     1.7 -  fix t t' :: typerep and ts
     1.8 -  have "(\<forall>t'. to_nat_typerep t = to_nat_typerep t' \<longrightarrow> t = t')
     1.9 -    \<and> (\<forall>ts'. map to_nat_typerep ts = map to_nat_typerep ts' \<longrightarrow> ts = ts')"
    1.10 -  proof (induct rule: typerep.induct)
    1.11 -    case (Typerep c ts) show ?case
    1.12 -    proof (rule allI, rule impI)
    1.13 -      fix t'
    1.14 -      assume hyp: "to_nat_typerep (Typerep.Typerep c ts) = to_nat_typerep t'"
    1.15 -      then obtain c' ts' where t': "t' = (Typerep.Typerep c' ts')"
    1.16 -        by (cases t') auto
    1.17 -      with Typerep hyp have "c = c'" and "ts = ts'" by simp_all
    1.18 -      with t' show "Typerep.Typerep c ts = t'" by simp
    1.19 -    qed
    1.20 +  fix t t' :: typerep and ts ts' :: "typerep list"
    1.21 +  assume "to_nat_typerep t = to_nat_typerep t'"
    1.22 +  moreover have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'"
    1.23 +    and "map to_nat_typerep ts = map to_nat_typerep ts' \<Longrightarrow> ts = ts'"
    1.24 +  proof (induct t and ts arbitrary: t' and ts' rule: typerep.inducts)
    1.25 +    case (Typerep c ts t')
    1.26 +    then obtain c' ts' where t': "t' = Typerep.Typerep c' ts'" by (cases t') auto
    1.27 +    with Typerep have "c = c'" and "ts = ts'" by simp_all
    1.28 +    with t' show "Typerep.Typerep c ts = t'" by simp
    1.29    next
    1.30      case Nil_typerep then show ?case by simp
    1.31    next
    1.32      case (Cons_typerep t ts) then show ?case by auto
    1.33    qed
    1.34 -  then have "to_nat_typerep t = to_nat_typerep t' \<Longrightarrow> t = t'" by auto
    1.35 -  moreover assume "to_nat_typerep t = to_nat_typerep t'"
    1.36    ultimately show "t = t'" by simp
    1.37  qed
    1.38