src/HOL/Library/Countable.thy
changeset 65411 3c628937899d
parent 63040 eb4ddd18d635
child 66453 cc19f7ca2ed6
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Apr 05 22:29:09 2017 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Wed Apr 05 19:23:41 2017 +0200
     1.3 @@ -176,7 +176,7 @@
     1.4            (case HOLogic.dest_Trueprop (Thm.concl_of typedef_thm) of
     1.5              (_ $ _ $ _ $ (_ $ Const (n, _))) => n
     1.6            | _ => raise Match)
     1.7 -        val induct_info = Inductive.the_inductive ctxt pred_name
     1.8 +        val induct_info = Inductive.the_inductive_global ctxt pred_name
     1.9          val pred_names = #names (fst induct_info)
    1.10          val induct_thms = #inducts (snd induct_info)
    1.11          val alist = pred_names ~~ induct_thms