diff -r cbc38731d42f -r 0fbed69ff081 src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Tue Mar 03 19:08:04 2015 +0100
+++ b/src/HOL/Library/Countable.thy	Wed Mar 04 19:53:18 2015 +0100
@@ -171,7 +171,7 @@
         val typedef_info = hd (Typedef.get_info ctxt ty_name)
         val typedef_thm = #type_definition (snd typedef_info)
         val pred_name =
-          (case HOLogic.dest_Trueprop (concl_of typedef_thm) of
+          (case HOLogic.dest_Trueprop (Thm.concl_of typedef_thm) of
             (_ $ _ $ _ $ (_ $ Const (n, _))) => n
           | _ => raise Match)
         val induct_info = Inductive.the_inductive ctxt pred_name