src/HOLCF/Tools/pcpodef_package.ML

     val full_name = full name;
     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
     val setT = Term.fastype_of set;
     val rhs_tfrees = term_tfrees set;
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
-      error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+      error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
     fun mk_nonempty A =
       HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
     fun mk_admissible A =
       mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
     fun mk_UU_mem A = HOLogic.mk_mem (Const ("Pcpo.UU", oldT), A);