changeset 56243 | 2e10a36b8d46 |
parent 55413 | a8e96847523c |
child 57437 | 0baf08c075b9 |
--- a/src/HOL/Library/Countable.thy Fri Mar 21 12:14:33 2014 +0100 +++ b/src/HOL/Library/Countable.thy Fri Mar 21 12:34:50 2014 +0100 @@ -275,7 +275,7 @@ let val ty_name = (case goal of - (_ $ Const (@{const_name TYPE}, Type (@{type_name itself}, [Type (n, _)]))) => n + (_ $ Const (@{const_name Pure.type}, Type (@{type_name itself}, [Type (n, _)]))) => n | _ => raise Match) val typedef_info = hd (Typedef.get_info ctxt ty_name) val typedef_thm = #type_definition (snd typedef_info)