src/HOL/Library/Countable.thy
changeset 67405 e9ab4ad7bd15
parent 67399 eab6ce8368fa
child 68028 1f9f973eed2a
     1.1 --- a/src/HOL/Library/Countable.thy	Thu Jan 11 12:32:07 2018 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Jan 11 13:48:17 2018 +0100
     1.3 @@ -180,7 +180,7 @@
     1.4          val pred_names = #names (fst induct_info)
     1.5          val induct_thms = #inducts (snd induct_info)
     1.6          val alist = pred_names ~~ induct_thms
     1.7 -        val induct_thm = the (AList.lookup (=) alist pred_name)
     1.8 +        val induct_thm = the (AList.lookup (op =) alist pred_name)
     1.9          val vars = rev (Term.add_vars (Thm.prop_of induct_thm) [])
    1.10          val insts = vars |> map (fn (_, T) => try (Thm.cterm_of ctxt)
    1.11            (Const (@{const_name Countable.finite_item}, T)))