src/HOLCF/Tools/pcpodef_package.ML

         val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
         val less_definition = singleton (ProofContext.export lthy4 ctxt_thy) less_definition';
         val thy5 = lthy4
           |> Class.prove_instantiation_instance
               (K (Tactic.rtac (typedef_po OF [type_definition, less_definition]) 1))
-          |> LocalTheory.exit
-          |> ProofContext.theory_of;
+          |> LocalTheory.exit_global;
       in ((type_definition, less_definition, set_def), thy5) end;
 
     fun make_cpo admissible (type_def, less_def, set_def) theory =
       let
         val admissible' = fold_rule (the_list set_def) admissible;