# HG changeset patch
# User blanchet
# Date 1411051660 -7200
# Node ID cf6f16bc11a7b5f8352a104ff8e32c904bb09be7
# Parent  c6f93b8d2d8e6cdafd1400100abe25045e70b0c1
use selector

diff -r c6f93b8d2d8e -r cf6f16bc11a7 src/HOL/Library/Phantom_Type.thy
--- a/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 16:47:40 2014 +0200
+++ b/src/HOL/Library/Phantom_Type.thy	Thu Sep 18 16:47:40 2014 +0200
@@ -8,13 +8,7 @@
 imports Main
 begin
 
-datatype ('a, 'b) phantom = phantom 'b
-
-primrec of_phantom :: "('a, 'b) phantom \<Rightarrow> 'b" 
-where "of_phantom (phantom x) = x"
-
-lemma of_phantom_phantom [simp]: "phantom (of_phantom x) = x"
-by(cases x) simp
+datatype ('a, 'b) phantom = phantom (of_phantom: 'b)
 
 lemma type_definition_phantom': "type_definition of_phantom phantom UNIV"
 by(unfold_locales) simp_all