# HG changeset patch # User kuncar # Date 1362745315 -3600 # Node ID 502f6a53519b9a41b0ea7147393ffb8eaf36e52d # Parent 7da251a6c16e57703f7d09528f4d4358c816ccd1 setup_lifting doesn't support a type variable as a raw type diff -r 7da251a6c16e -r 502f6a53519b src/HOL/Library/Phantom_Type.thy --- a/src/HOL/Library/Phantom_Type.thy Fri Mar 08 13:21:52 2013 +0100 +++ b/src/HOL/Library/Phantom_Type.thy Fri Mar 08 13:21:55 2013 +0100 @@ -17,8 +17,6 @@ lemma type_definition_phantom': "type_definition of_phantom phantom UNIV" by(unfold_locales) simp_all -setup_lifting (no_code) type_definition_phantom' - lemma phantom_comp_of_phantom [simp]: "phantom \ of_phantom = id" and of_phantom_comp_phantom [simp]: "of_phantom \ phantom = id" by(simp_all add: o_def id_def)