src/Pure/Proof/proof_syntax.ML
changeset 15531 08c8dad8e399
parent 14981 e73f8140af78
child 15570 8d8c70b41bab
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -133,41 +133,41 @@
     1.4  
     1.5      fun prf_of [] (Bound i) = PBound i
     1.6        | prf_of Ts (Const (s, Type ("proof", _))) =
     1.7 -          change_type (if ty then Some Ts else None)
     1.8 +          change_type (if ty then SOME Ts else NONE)
     1.9              (case NameSpace.unpack s of
    1.10                 "axm" :: xs =>
    1.11                   let
    1.12                     val name = NameSpace.pack xs;
    1.13                     val prop = (case assoc (axms, name) of
    1.14 -                       Some prop => prop
    1.15 -                     | None => error ("Unknown axiom " ^ quote name))
    1.16 -                 in PAxm (name, prop, None) end
    1.17 +                       SOME prop => prop
    1.18 +                     | NONE => error ("Unknown axiom " ^ quote name))
    1.19 +                 in PAxm (name, prop, NONE) end
    1.20               | "thm" :: xs =>
    1.21                   let val name = NameSpace.pack xs;
    1.22                   in (case assoc (thms, name) of
    1.23 -                     Some thm => fst (strip_combt (Thm.proof_of thm))
    1.24 -                   | None => (case Symtab.lookup (tab, name) of
    1.25 -                         Some prf => prf
    1.26 -                       | None => error ("Unknown theorem " ^ quote name)))
    1.27 +                     SOME thm => fst (strip_combt (Thm.proof_of thm))
    1.28 +                   | NONE => (case Symtab.lookup (tab, name) of
    1.29 +                         SOME prf => prf
    1.30 +                       | NONE => error ("Unknown theorem " ^ quote name)))
    1.31                   end
    1.32               | _ => error ("Illegal proof constant name: " ^ quote s))
    1.33        | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
    1.34        | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
    1.35        | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
    1.36 -          Abst (s, if ty then Some T else None,
    1.37 +          Abst (s, if ty then SOME T else NONE,
    1.38              incr_pboundvars (~1) 0 (prf_of [] prf))
    1.39        | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
    1.40            AbsP (s, case t of
    1.41 -                Const ("dummy_pattern", _) => None
    1.42 -              | _ $ Const ("dummy_pattern", _) => None
    1.43 -              | _ => Some (mk_term t),
    1.44 +                Const ("dummy_pattern", _) => NONE
    1.45 +              | _ $ Const ("dummy_pattern", _) => NONE
    1.46 +              | _ => SOME (mk_term t),
    1.47              incr_pboundvars 0 (~1) (prf_of [] prf))
    1.48        | prf_of [] (Const ("AppP", _) $ prf1 $ prf2) =
    1.49            prf_of [] prf1 %% prf_of [] prf2
    1.50        | prf_of Ts (Const ("Appt", _) $ prf $ Const ("TYPE", Type (_, [T]))) =
    1.51            prf_of (T::Ts) prf
    1.52        | prf_of [] (Const ("Appt", _) $ prf $ t) = prf_of [] prf %
    1.53 -          (case t of Const ("dummy_pattern", _) => None | _ => Some (mk_term t))
    1.54 +          (case t of Const ("dummy_pattern", _) => NONE | _ => SOME (mk_term t))
    1.55        | prf_of _ t = error ("Not a proof term:\n" ^
    1.56            Sign.string_of_term (sign_of thy) t)
    1.57  
    1.58 @@ -183,12 +183,12 @@
    1.59  val mk_tyapp = foldl (fn (prf, T) => Const ("Appt",
    1.60    [proofT, itselfT T] ---> proofT) $ prf $ Logic.mk_type T);
    1.61  
    1.62 -fun term_of _ (PThm ((name, _), _, _, None)) =
    1.63 +fun term_of _ (PThm ((name, _), _, _, NONE)) =
    1.64        Const (add_prefix "thm" name, proofT)
    1.65 -  | term_of _ (PThm ((name, _), _, _, Some Ts)) =
    1.66 +  | term_of _ (PThm ((name, _), _, _, SOME Ts)) =
    1.67        mk_tyapp (Const (add_prefix "thm" name, proofT), Ts)
    1.68 -  | term_of _ (PAxm (name, _, None)) = Const (add_prefix "axm" name, proofT)
    1.69 -  | term_of _ (PAxm (name, _, Some Ts)) =
    1.70 +  | term_of _ (PAxm (name, _, NONE)) = Const (add_prefix "axm" name, proofT)
    1.71 +  | term_of _ (PAxm (name, _, SOME Ts)) =
    1.72        mk_tyapp (Const (add_prefix "axm" name, proofT), Ts)
    1.73    | term_of _ (PBound i) = Bound i
    1.74    | term_of Ts (Abst (s, opT, prf)) =