1.1 --- a/src/HOL/Library/Countable.thy	Sat Mar 17 17:44:29 2012 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Sat Mar 17 17:58:40 2012 +0100
     1.3 @@ -276,7 +276,7 @@
     1.4        let
     1.5          val ty_name =
     1.6            (case goal of
     1.7 -            (_ $ Const ("TYPE", Type ("itself", [Type (n, _)]))) => n
     1.8 +            (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n
     1.9            | _ => raise Match)
    1.10          val typedef_info = hd (Typedef.get_info ctxt ty_name)
    1.11          val typedef_thm = #type_definition (snd typedef_info)