src/HOL/Library/Countable.thy
changeset 60801 7664e0916eec
parent 60752 b48830b670a1
child 61076 bdc1e2f0a86a
     1.1 --- a/src/HOL/Library/Countable.thy	Mon Jul 27 16:35:12 2015 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Mon Jul 27 17:44:55 2015 +0200
     1.3 @@ -182,7 +182,7 @@
     1.4          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
     1.5          val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
     1.6            (Const (@{const_name Countable.finite_item}, T)))
     1.7 -        val induct_thm' = Drule.instantiate' [] insts induct_thm
     1.8 +        val induct_thm' = Thm.instantiate' [] insts induct_thm
     1.9          val rules = @{thms finite_item.intros}
    1.10        in
    1.11          SOLVED' (fn i => EVERY