--- 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