src/HOLCF/Tools/repdef.ML

       [type_definition_thm, #below_def cpo_info, emb_def, prj_def];
     val ([REP_thm], thy5) = thy4
       |> Sign.add_path (Binding.name_of name)
       |> PureThy.add_thms
         [((Binding.prefix_name "REP_" name,
-          Drule.standard (@{thm typedef_REP} OF typedef_thms')), [])]
+          Drule.export_without_context (@{thm typedef_REP} OF typedef_thms')), [])]
       ||> Sign.parent_path;
 
     val rep_info =
       { emb_def = emb_def, prj_def = prj_def, approx_def = approx_def, REP = REP_thm };
   in