src/HOL/HOLCF/Tools/cpodef.ML

           ((Binding.prefix_name "below_" (Thm.def_binding name), []), below_eqn)
     val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy)
     val below_def = singleton (Proof_Context.export lthy ctxt_thy) below_ldef
     val thy = lthy
       |> Class.prove_instantiation_exit
-          (fn ctxt => resolve_tac ctxt [@{thm typedef_po} OF [type_definition, below_def]] 1)
+          (fn ctxt => resolve_tac ctxt [@{thm typedef_po_class} OF [type_definition, below_def]] 1)
   in ((info, below_def), thy) end
 
 fun prepare_cpodef
       (prep_term: Proof.context -> 'a -> term)
       (typ: binding * (string * sort) list * mixfix)