Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more antiquotations;
authorwenzelm
Sat, 17 Mar 2012 17:58:40 +0100
changeset 46998 11b38c94b21a
parent 46997 395b7277ed76
child 46999 1c3c185bab4e
more antiquotations;
src/HOL/Library/Countable.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle