merged

--- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 19:01:50 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Fri Sep 19 08:26:03 2014 +0200
@@ -30,4 +30,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