src/HOL/Tools/Lifting/lifting_def_code_dt.ML

     fun R_conv rel_eq_onps = Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}
       then_conv Transfer.bottom_rewr_conv rel_eq_onps
 
     val (ret_lift_def, lthy) = add_lift_def (#lift_config config) var qty rhs rsp_thm par_thms lthy
   in
-    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ))
+    if (not (#code_dt config) orelse (code_eq_of_lift_def ret_lift_def <> NONE_EQ)
+      andalso (code_eq_of_lift_def ret_lift_def <> UNKNOWN_EQ))
+      (* Let us try even in case of UNKNOWN_EQ. If this leads to problems, the user can always
+        say that they do not want this workaround. *)
     then  (ret_lift_def, lthy)
     else
       let
         val lift_def = inst_of_lift_def lthy qty ret_lift_def
         val rty = rty_of_lift_def lift_def