src/HOLCF/pcpodef_package.ML

 fun read_term thy used s =
   #1 (Thm.read_def_cterm (thy, K NONE, K NONE) used true (s, HOLogic.typeT));
 
 fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
 
-fun err_in_cpodef name =
-  error ("The error(s) above occurred in cpodef " ^ quote name);
+fun err_in_cpodef msg name =
+  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
 
 fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
 
 fun gen_prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =

         |> make_cpo admissible
         |> (fn (theory', (type_def, _, _)) => (theory', type_def))
       end;
   
   in (goal, if pcpo then pcpodef_result else cpodef_result) end
-  handle ERROR => err_in_cpodef name;
+  handle ERROR msg => err_in_cpodef msg name;
 
 (* cpodef_proof interface *)
 
 fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
   let