src/HOLCF/Tools/repdef.ML

       prj_def : thm,
       defl_def : thm,
       liftemb_def : thm,
       liftprj_def : thm,
       liftdefl_def : thm,
-      DEFL : thm,
-      LIFTDEFL : thm
+      DEFL : thm
     }
 
   val add_repdef: bool -> binding option -> binding * (string * sort) list * mixfix ->
     term -> (binding * binding) option -> theory ->
     (Typedef.info * Pcpodef.cpo_info * Pcpodef.pcpo_info * rep_info) * theory

     prj_def : thm,
     defl_def : thm,
     liftemb_def : thm,
     liftprj_def : thm,
     liftdefl_def : thm,
-    DEFL : thm,
-    LIFTDEFL : thm
+    DEFL : thm
   };
 
 (* building types and terms *)
 
 val udomT = @{typ udom};

     val liftprj_bind = (Binding.prefix_name "liftprj_" name_def, []);
     val liftdefl_bind = (Binding.prefix_name "liftdefl_" name_def, []);
 
     (*instantiate class rep*)
     val lthy = thy
-      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort bifinite});
+      |> Class.instantiation ([full_tname], lhs_tfrees, @{sort liftdomain});
     val ((_, (_, emb_ldef)), lthy) =
         Specification.definition (NONE, (emb_bind, emb_eqn)) lthy;
     val ((_, (_, prj_ldef)), lthy) =
         Specification.definition (NONE, (prj_bind, prj_eqn)) lthy;
     val ((_, (_, defl_ldef)), lthy) =

           (K (Tactic.rtac (@{thm typedef_rep_class} OF typedef_thms) 1))
       |> Local_Theory.exit_global;
 
     (*other theorems*)
     val defl_thm' = Thm.transfer thy defl_def;
-    val liftdefl_thm' = Thm.transfer thy liftdefl_def;
     val (DEFL_thm, thy) = thy
       |> Sign.add_path (Binding.name_of name)
       |> Global_Theory.add_thm
          ((Binding.prefix_name "DEFL_" name,
           Drule.zero_var_indexes (@{thm typedef_DEFL} OF [defl_thm'])), [])
       ||> Sign.restore_naming thy;
-    val (LIFTDEFL_thm, thy) = thy
-      |> Sign.add_path (Binding.name_of name)
-      |> Global_Theory.add_thm
-         ((Binding.prefix_name "LIFTDEFL_" name,
-          Drule.zero_var_indexes (@{thm typedef_LIFTDEFL} OF [liftdefl_thm'])), [])
-      ||> Sign.restore_naming thy;
 
     val rep_info =
       { emb_def = emb_def, prj_def = prj_def, defl_def = defl_def,
         liftemb_def = liftemb_def, liftprj_def = liftprj_def,
-        liftdefl_def = liftdefl_def,
-        DEFL = DEFL_thm, LIFTDEFL = LIFTDEFL_thm };
+        liftdefl_def = liftdefl_def, DEFL = DEFL_thm };
   in
     ((info, cpo_info, pcpo_info, rep_info), thy)
   end
   handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in repdef " ^ quote (Binding.str_of name));