error -> raise Fail
authorhuffman
Mon, 22 Mar 2010 15:53:25 -0700
changeset 35912 b0e300bd3a2c
parent 35908 21e45c81e828
child 35913 6943a36453e8
error -> raise Fail
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/holcf_library.ML
src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 15:45:54 2010 -0700
+++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 15:53:25 2010 -0700
@@ -212,7 +212,7 @@
 fun con_app2 con f args = list_ccomb(%%:con,map f args);
 fun con_app con = con_app2 con %#;
 fun prj _  _  x (   _::[]) _ = x
-  | prj _  _  _ []         _ = error "Domain_Library.prj: empty list"
+  | prj _  _  _ []         _ = raise Fail "Domain_Library.prj: empty list"
   | prj f1 _  x (_::y::ys) 0 = f1 x y
   | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
 fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
--- a/src/HOLCF/Tools/holcf_library.ML	Mon Mar 22 15:45:54 2010 -0700
+++ b/src/HOLCF/Tools/holcf_library.ML	Mon Mar 22 15:53:25 2010 -0700
@@ -227,7 +227,7 @@
       in
         (v::vs, mk_ssumT (T, U))
       end
-    fun inj [] = error "mk_sinjects: empty list"
+    fun inj [] = raise Fail "mk_sinjects: empty list"
       | inj ((t, T)::[]) = ([t], T)
       | inj ((t, T)::ts) = combine (t, T) (inj ts);
   in
--- a/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 15:45:54 2010 -0700
+++ b/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 15:53:25 2010 -0700
@@ -327,7 +327,7 @@
     val (goal1, goal2, make_result) =
       prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
-      | after_qed _ = error "cpodef_proof";
+      | after_qed _ = raise Fail "cpodef_proof";
   in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 fun gen_pcpodef_proof prep_term prep_constraint
@@ -338,7 +338,7 @@
     val (goal1, goal2, make_result) =
       prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
     fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
-      | after_qed _ = error "pcpodef_proof";
+      | after_qed _ = raise Fail "pcpodef_proof";
   in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
 
 in