add lemma

--- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 00:03:46 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 15:23:23 2014 +0200
@@ -36,4 +36,8 @@
   in [(@{const_syntax phantom}, phantom_tr')] end
 *}
 
+lemma of_phantom_inject [simp]:
+  "of_phantom x = of_phantom y \<longleftrightarrow> x = y"
+by(cases x y rule: phantom.exhaust[case_product phantom.exhaust]) simp
+
 end