src/HOLCF/pcpodef_package.ML
changeset 18678 dd0c569fa43d
parent 18377 0e1d025d57b3
child 18728 6790126ab5f6
     1.1 --- a/src/HOLCF/pcpodef_package.ML	Fri Jan 13 17:39:41 2006 +0100
     1.2 +++ b/src/HOLCF/pcpodef_package.ML	Sat Jan 14 17:14:06 2006 +0100
     1.3 @@ -53,8 +53,8 @@
     1.4  
     1.5  fun cert_term thy _ t = Thm.cterm_of thy t handle TERM (msg, _) => error msg;
     1.6  
     1.7 -fun err_in_cpodef name =
     1.8 -  error ("The error(s) above occurred in cpodef " ^ quote name);
     1.9 +fun err_in_cpodef msg name =
    1.10 +  cat_error msg ("The error(s) above occurred in cpodef " ^ quote name);
    1.11  
    1.12  fun adm_const T = Const ("Adm.adm", (T --> HOLogic.boolT) --> HOLogic.boolT);
    1.13  fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
    1.14 @@ -168,7 +168,7 @@
    1.15        end;
    1.16    
    1.17    in (goal, if pcpo then pcpodef_result else cpodef_result) end
    1.18 -  handle ERROR => err_in_cpodef name;
    1.19 +  handle ERROR msg => err_in_cpodef msg name;
    1.20  
    1.21  (* cpodef_proof interface *)
    1.22