Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Phantom_Type.thy
changeset 69593 3dda49e08b9d
parent 60500 903bb1495239 
--- a/src/HOL/Library/Phantom_Type.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Library/Phantom_Type.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -23,11 +23,11 @@
 
 typed_print_translation \<open>
   let
-    fun phantom_tr' ctxt (Type (@{type_name fun}, [_, Type (@{type_name phantom}, [T, _])])) ts =
+    fun phantom_tr' ctxt (Type (\<^type_name>\<open>fun\<close>, [_, Type (\<^type_name>\<open>phantom\<close>, [T, _])])) ts =
           list_comb
-            (Syntax.const @{syntax_const "_Phantom"} $ Syntax_Phases.term_of_typ ctxt T, ts)
+            (Syntax.const \<^syntax_const>\<open>_Phantom\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
       | phantom_tr' _ _ _ = raise Match;
-  in [(@{const_syntax phantom}, phantom_tr')] end
+  in [(\<^const_syntax>\<open>phantom\<close>, phantom_tr')] end
 \<close>
 
 lemma of_phantom_inject [simp]:
isabelle