# HG changeset patch
# User wenzelm
# Date 1332003520 -3600
# Node ID 11b38c94b21ab5e98442b0cf96e631a649cac44a
# Parent  395b7277ed76c45edd2636c63926f506b4bed2cd
more antiquotations;

diff -r 395b7277ed76 -r 11b38c94b21a src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Sat Mar 17 17:44:29 2012 +0100
+++ b/src/HOL/Library/Countable.thy	Sat Mar 17 17:58:40 2012 +0100
@@ -276,7 +276,7 @@
       let
         val ty_name =
           (case goal of
-            (_ $ Const ("TYPE", Type ("itself", [Type (n, _)]))) => n
+            (_ $ Const (@{const_name 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)