src/ZF/arith_data.ML
changeset 15531 08c8dad8e399
parent 14387 e96d5c42c4b0
child 15570 8d8c70b41bab
     1.1 --- a/src/ZF/arith_data.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/ZF/arith_data.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -53,8 +53,8 @@
     1.4    | dest_sum tm = [tm];
     1.5  
     1.6  (*Apply the given rewrite (if present) just once*)
     1.7 -fun gen_trans_tac th2 None      = all_tac
     1.8 -  | gen_trans_tac th2 (Some th) = ALLGOALS (rtac (th RS th2));
     1.9 +fun gen_trans_tac th2 NONE      = all_tac
    1.10 +  | gen_trans_tac th2 (SOME th) = ALLGOALS (rtac (th RS th2));
    1.11  
    1.12  (*Use <-> or = depending on the type of t*)
    1.13  fun mk_eq_iff(t,u) =
    1.14 @@ -69,14 +69,14 @@
    1.15  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
    1.16  
    1.17  fun prove_conv name tacs sg hyps xs (t,u) =
    1.18 -  if t aconv u then None
    1.19 +  if t aconv u then NONE
    1.20    else
    1.21    let val hyps' = filter (not o is_eq_thm) hyps
    1.22        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    1.23          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    1.24 -  in Some (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
    1.25 +  in SOME (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
    1.26        handle ERROR_MESSAGE msg =>
    1.27 -        (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
    1.28 +        (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
    1.29    end;
    1.30  
    1.31  fun prep_simproc (name, pats, proc) =