error -> raise Fail
authorhuffman
Mon Mar 22 15:53:25 2010 -0700 (2010-03-22)
changeset 35912b0e300bd3a2c
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
     1.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 15:45:54 2010 -0700
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Mon Mar 22 15:53:25 2010 -0700
     1.3 @@ -212,7 +212,7 @@
     1.4  fun con_app2 con f args = list_ccomb(%%:con,map f args);
     1.5  fun con_app con = con_app2 con %#;
     1.6  fun prj _  _  x (   _::[]) _ = x
     1.7 -  | prj _  _  _ []         _ = error "Domain_Library.prj: empty list"
     1.8 +  | prj _  _  _ []         _ = raise Fail "Domain_Library.prj: empty list"
     1.9    | prj f1 _  x (_::y::ys) 0 = f1 x y
    1.10    | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    1.11  fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
     2.1 --- a/src/HOLCF/Tools/holcf_library.ML	Mon Mar 22 15:45:54 2010 -0700
     2.2 +++ b/src/HOLCF/Tools/holcf_library.ML	Mon Mar 22 15:53:25 2010 -0700
     2.3 @@ -227,7 +227,7 @@
     2.4        in
     2.5          (v::vs, mk_ssumT (T, U))
     2.6        end
     2.7 -    fun inj [] = error "mk_sinjects: empty list"
     2.8 +    fun inj [] = raise Fail "mk_sinjects: empty list"
     2.9        | inj ((t, T)::[]) = ([t], T)
    2.10        | inj ((t, T)::ts) = combine (t, T) (inj ts);
    2.11    in
     3.1 --- a/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 15:45:54 2010 -0700
     3.2 +++ b/src/HOLCF/Tools/pcpodef.ML	Mon Mar 22 15:53:25 2010 -0700
     3.3 @@ -327,7 +327,7 @@
     3.4      val (goal1, goal2, make_result) =
     3.5        prepare_cpodef prep_term def name (b, args, mx) set opt_morphs thy;
     3.6      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
     3.7 -      | after_qed _ = error "cpodef_proof";
     3.8 +      | after_qed _ = raise Fail "cpodef_proof";
     3.9    in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    3.10  
    3.11  fun gen_pcpodef_proof prep_term prep_constraint
    3.12 @@ -338,7 +338,7 @@
    3.13      val (goal1, goal2, make_result) =
    3.14        prepare_pcpodef prep_term def name (b, args, mx) set opt_morphs thy;
    3.15      fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2)
    3.16 -      | after_qed _ = error "pcpodef_proof";
    3.17 +      | after_qed _ = raise Fail "pcpodef_proof";
    3.18    in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] ctxt end;
    3.19  
    3.20  in