src/HOL/Library/Float.thy

 end
 
 lemma type_definition_float': "type_definition real float_of float"
   using type_definition_float unfolding real_of_float_def .
 
-setup_lifting (no_code) type_definition_float'
+setup_lifting type_definition_float'
 
 lemmas float_of_inject[simp]
 
 declare [[coercion "real :: float \<Rightarrow> real"]]