src/Pure/drule.ML
changeset 15531 08c8dad8e399
parent 15495 50fde6f04e4c
child 15545 0efa7126003f
     1.1 --- a/src/Pure/drule.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/drule.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -223,15 +223,15 @@
     1.4        (case Symbol.explode a of "'" :: _ => true | _ => false);
     1.5      val (tvs, vs) = partition is_tv insts;
     1.6      fun readT (ixn, st) =
     1.7 -        let val S = case rsorts ixn of Some S => S | None => absent ixn;
     1.8 +        let val S = case rsorts ixn of SOME S => S | NONE => absent ixn;
     1.9              val T = Sign.read_typ (sign,sorts) st;
    1.10          in if Sign.typ_instance sign (T, TVar(ixn,S)) then (ixn,T)
    1.11             else inst_failure ixn
    1.12          end
    1.13      val tye = map readT tvs;
    1.14      fun mkty(ixn,st) = (case rtypes ixn of
    1.15 -                          Some T => (ixn,(st,typ_subst_TVars tye T))
    1.16 -                        | None => absent ixn);
    1.17 +                          SOME T => (ixn,(st,typ_subst_TVars tye T))
    1.18 +                        | NONE => absent ixn);
    1.19      val ixnsTs = map mkty vs;
    1.20      val ixns = map fst ixnsTs
    1.21      and sTs  = map snd ixnsTs
    1.22 @@ -294,7 +294,7 @@
    1.23  
    1.24  fun get_kind thm =
    1.25    (case Library.assoc (#2 (Thm.get_name_tags thm), "kind") of
    1.26 -    Some (k :: _) => k
    1.27 +    SOME (k :: _) => k
    1.28    | _ => "unknown");
    1.29  
    1.30  fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind";
    1.31 @@ -667,7 +667,7 @@
    1.32    let val p as (ct1, ct2) = Thm.dest_comb ct
    1.33    in (case pairself term_of p of
    1.34        (Const ("all", _), Abs (s, _, _)) =>
    1.35 -         let val (v, ct') = Thm.dest_abs (Some "@") ct2;
    1.36 +         let val (v, ct') = Thm.dest_abs (SOME "@") ct2;
    1.37           in Thm.combination (Thm.reflexive ct1)
    1.38             (Thm.abstract_rule s v (forall_conv cv ct'))
    1.39           end
    1.40 @@ -677,7 +677,7 @@
    1.41  (*Use a conversion to transform a theorem*)
    1.42  fun fconv_rule cv th = equal_elim (cv (cprop_of th)) th;
    1.43  
    1.44 -(*** Some useful meta-theorems ***)
    1.45 +(*** SOME useful meta-theorems ***)
    1.46  
    1.47  (*The rule V/V, obtains assumption solving for eresolve_tac*)
    1.48  val asm_rl = store_standard_thm_open "asm_rl" (Thm.trivial (read_prop "PROP ?psi"));
    1.49 @@ -913,8 +913,8 @@
    1.50          handle TYPE (msg, _, _) => err msg;
    1.51  
    1.52      fun zip_vars _ [] = []
    1.53 -      | zip_vars (_ :: vs) (None :: opt_ts) = zip_vars vs opt_ts
    1.54 -      | zip_vars (v :: vs) (Some t :: opt_ts) = (v, t) :: zip_vars vs opt_ts
    1.55 +      | zip_vars (_ :: vs) (NONE :: opt_ts) = zip_vars vs opt_ts
    1.56 +      | zip_vars (v :: vs) (SOME t :: opt_ts) = (v, t) :: zip_vars vs opt_ts
    1.57        | zip_vars [] _ = err "more instantiations than variables in thm";
    1.58  
    1.59      (*instantiate types first!*)
    1.60 @@ -972,14 +972,14 @@
    1.61  fun unvarifyT thm =
    1.62    let
    1.63      val cT = Thm.ctyp_of (Thm.sign_of_thm thm);
    1.64 -    val tfrees = map (fn ((x, _), S) => Some (cT (TFree (x, S)))) (tvars_of thm);
    1.65 +    val tfrees = map (fn ((x, _), S) => SOME (cT (TFree (x, S)))) (tvars_of thm);
    1.66    in instantiate' tfrees [] thm end;
    1.67  
    1.68  fun unvarify raw_thm =
    1.69    let
    1.70      val thm = unvarifyT raw_thm;
    1.71      val ct = Thm.cterm_of (Thm.sign_of_thm thm);
    1.72 -    val frees = map (fn ((x, _), T) => Some (ct (Free (x, T)))) (vars_of thm);
    1.73 +    val frees = map (fn ((x, _), T) => SOME (ct (Free (x, T)))) (vars_of thm);
    1.74    in instantiate' [] frees thm end;
    1.75  
    1.76  
    1.77 @@ -1014,14 +1014,14 @@
    1.78      [] => thm
    1.79    | tvars =>
    1.80        let val cert = Thm.ctyp_of (Thm.sign_of_thm thm)
    1.81 -      in instantiate' (map (fn ((x, _), S) => Some (cert (TFree (x, S)))) tvars) [] thm end);
    1.82 +      in instantiate' (map (fn ((x, _), S) => SOME (cert (TFree (x, S)))) tvars) [] thm end);
    1.83  
    1.84  fun freeze_all_Vars thm =
    1.85    (case vars_of thm of
    1.86      [] => thm
    1.87    | vars =>
    1.88        let val cert = Thm.cterm_of (Thm.sign_of_thm thm)
    1.89 -      in instantiate' [] (map (fn ((x, _), T) => Some (cert (Free (x, T)))) vars) thm end);
    1.90 +      in instantiate' [] (map (fn ((x, _), T) => SOME (cert (Free (x, T)))) vars) thm end);
    1.91  
    1.92  val freeze_all = freeze_all_Vars o freeze_all_TVars;
    1.93  
    1.94 @@ -1029,7 +1029,7 @@
    1.95  (* mk_triv_goal *)
    1.96  
    1.97  (*make an initial proof state, "PROP A ==> (PROP A)" *)
    1.98 -fun mk_triv_goal ct = instantiate' [] [Some ct] triv_goal;
    1.99 +fun mk_triv_goal ct = instantiate' [] [SOME ct] triv_goal;
   1.100  
   1.101  
   1.102