standardized basic operations on type option;
authorwenzelm
Wed Oct 21 00:36:12 2009 +0200 (2009-10-21)
changeset 3303515eab423e573
parent 33034 66ef64a5f122
child 33036 c61fe520602b
standardized basic operations on type option;
src/HOL/Import/proof_kernel.ML
src/HOL/Import/replay.ML
src/HOL/Library/Numeral_Type.thy
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Modelcheck/MuckeSyn.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/cnf_funcs.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/metis_tools.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_hol_clause.ML
src/HOL/Tools/res_reconstruct.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/sat_solver.ML
src/Pure/ProofGeneral/pgip_output.ML
src/Pure/ProofGeneral/pgml.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -583,7 +583,7 @@
     1.4  
     1.5  fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
     1.6      let
     1.7 -        val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
     1.8 +        val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[])))
     1.9          fun IT _ [] = ()
    1.10            | IT n (xty::xtys) =
    1.11              (Array.update(types,n,XMLty xty);
    1.12 @@ -650,7 +650,7 @@
    1.13  
    1.14  fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
    1.15      let
    1.16 -        val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
    1.17 +        val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[])))
    1.18  
    1.19          fun IT _ [] = ()
    1.20            | IT n (xtm::xtms) =
    1.21 @@ -1239,7 +1239,7 @@
    1.22          val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
    1.23      in
    1.24          if not (idx = "") andalso u = "_"
    1.25 -        then SOME (newstr,valOf(Int.fromString idx))
    1.26 +        then SOME (newstr, the (Int.fromString idx))
    1.27          else NONE
    1.28      end
    1.29      handle _ => NONE  (* FIXME avoid handle _ *)
    1.30 @@ -1914,7 +1914,7 @@
    1.31  fun new_definition thyname constname rhs thy =
    1.32      let
    1.33          val constname = rename_const thyname thy constname
    1.34 -        val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
    1.35 +        val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname));
    1.36          val _ = warning ("Introducing constant " ^ constname)
    1.37          val (thmname,thy) = get_defname thyname constname thy
    1.38          val (info,rhs') = disamb_term rhs
     2.1 --- a/src/HOL/Import/replay.ML	Tue Oct 20 23:25:04 2009 +0200
     2.2 +++ b/src/HOL/Import/replay.ML	Wed Oct 21 00:36:12 2009 +0200
     2.3 @@ -291,7 +291,7 @@
     2.4                  fun get_facts facts =
     2.5                      case TextIO.inputLine is of
     2.6                          NONE => (case facts of
     2.7 -                                   i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
     2.8 +                                   i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
     2.9                                   | _ => raise ERR "replay_thm" "Bad facts.lst file")
    2.10                        | SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
    2.11              in
     3.1 --- a/src/HOL/Library/Numeral_Type.thy	Tue Oct 20 23:25:04 2009 +0200
     3.2 +++ b/src/HOL/Library/Numeral_Type.thy	Wed Oct 21 00:36:12 2009 +0200
     3.3 @@ -408,7 +408,7 @@
     3.4    in bin_of n end;
     3.5  
     3.6  fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
     3.7 -      mk_bintype (valOf (Int.fromString str))
     3.8 +      mk_bintype (the (Int.fromString str))
     3.9    | numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
    3.10  
    3.11  in [("_NumeralType", numeral_tr)] end;
     4.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Oct 20 23:25:04 2009 +0200
     4.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Wed Oct 21 00:36:12 2009 +0200
     4.3 @@ -520,7 +520,7 @@
     4.4  fun rat_of_quotient (a,b) = if b = 0 then rat_0 else Rat.rat_of_quotient (a,b);
     4.5  fun rat_of_string s =
     4.6   let val n = index_char s #"/" 0 in
     4.7 -  if n = ~1 then s |> Int.fromString |> valOf |> Rat.rat_of_int
     4.8 +  if n = ~1 then s |> Int.fromString |> the |> Rat.rat_of_int
     4.9    else
    4.10     let val SOME numer = Int.fromString(String.substring(s,0,n))
    4.11         val SOME den = Int.fromString (String.substring(s,n+1,String.size s - n - 1))
    4.12 @@ -1193,7 +1193,7 @@
    4.13  fun real_nonlinear_prover proof_method ctxt =
    4.14   let
    4.15    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.16 -      (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    4.17 +      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    4.18       simple_cterm_ord
    4.19    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
    4.20         real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
    4.21 @@ -1308,7 +1308,7 @@
    4.22  fun real_nonlinear_subst_prover prover ctxt =
    4.23   let
    4.24    val {add,mul,neg,pow,sub,main} =  Normalizer.semiring_normalizers_ord_wrapper ctxt
    4.25 -      (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    4.26 +      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    4.27       simple_cterm_ord
    4.28  
    4.29    val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
     5.1 --- a/src/HOL/Library/normarith.ML	Tue Oct 20 23:25:04 2009 +0200
     5.2 +++ b/src/HOL/Library/normarith.ML	Wed Oct 21 00:36:12 2009 +0200
     5.3 @@ -167,7 +167,7 @@
     5.4    (* FIXME : Should be computed statically!! *)
     5.5    val real_poly_conv = 
     5.6      Normalizer.semiring_normalize_wrapper ctxt
     5.7 -     (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
     5.8 +     (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
     5.9   in fconv_rule (arg_conv ((rewr_conv @{thm ge_iff_diff_ge_0}) then_conv arg_conv (field_comp_conv then_conv real_poly_conv)))
    5.10  end;
    5.11  
    5.12 @@ -278,7 +278,7 @@
    5.13     (* FIXME: Should be computed statically!!*)
    5.14     val real_poly_conv = 
    5.15        Normalizer.semiring_normalize_wrapper ctxt
    5.16 -       (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    5.17 +       (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
    5.18     val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
    5.19     val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) [] 
    5.20     val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check" 
    5.21 @@ -384,7 +384,7 @@
    5.22    let 
    5.23     val real_poly_neg_conv = #neg
    5.24         (Normalizer.semiring_normalizers_ord_wrapper ctxt
    5.25 -        (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    5.26 +        (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
    5.27     val (th1,th2) = conj_pair(rawrule th)
    5.28    in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
    5.29    end
     6.1 --- a/src/HOL/Library/positivstellensatz.ML	Tue Oct 20 23:25:04 2009 +0200
     6.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Oct 21 00:36:12 2009 +0200
     6.3 @@ -43,7 +43,7 @@
     6.4    in Tab.fold h a b end;
     6.5  
     6.6  fun choose f = case Tab.min_key f of 
     6.7 -   SOME k => (k,valOf (Tab.lookup f k))
     6.8 +   SOME k => (k, the (Tab.lookup f k))
     6.9   | NONE => error "FuncFun.choose : Completely empty function"
    6.10  
    6.11  fun onefunc kv = update kv empty
    6.12 @@ -743,7 +743,7 @@
    6.13    fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
    6.14    val {add,mul,neg,pow,sub,main} = 
    6.15       Normalizer.semiring_normalizers_ord_wrapper ctxt
    6.16 -      (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
    6.17 +      (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) 
    6.18       simple_cterm_ord
    6.19  in gen_real_arith ctxt
    6.20     (cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
     7.1 --- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Oct 20 23:25:04 2009 +0200
     7.2 +++ b/src/HOL/Modelcheck/MuckeSyn.thy	Wed Oct 21 00:36:12 2009 +0200
     7.3 @@ -123,8 +123,8 @@
     7.4                       REPEAT (resolve_tac prems 1)]);
     7.5  
     7.6    val sig_move_thm = Thm.theory_of_thm move_thm;
     7.7 -  val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
     7.8 -  val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm)))); 
     7.9 +  val bCterm = cterm_of sig_move_thm (the (search_var "b" (concl_of move_thm)));
    7.10 +  val aCterm = cterm_of sig_move_thm (the (search_var "a" (hd(prems_of move_thm)))); 
    7.11  
    7.12  in
    7.13  
     8.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Tue Oct 20 23:25:04 2009 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Oct 21 00:36:12 2009 +0200
     8.3 @@ -50,7 +50,7 @@
     8.4  
     8.5  fun dt_cases (descr: descr) (_, args, constrs) =
     8.6    let
     8.7 -    fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
     8.8 +    fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
     8.9      val bnames = map the_bname (distinct op = (maps dt_recs args));
    8.10    in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
    8.11  
    8.12 @@ -58,7 +58,7 @@
    8.13  fun induct_cases descr =
    8.14    DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
    8.15  
    8.16 -fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
    8.17 +fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
    8.18  
    8.19  in
    8.20  
    8.21 @@ -233,7 +233,7 @@
    8.22      fun replace_types (Type ("Nominal.ABS", [T, U])) =
    8.23            Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
    8.24        | replace_types (Type (s, Ts)) =
    8.25 -          Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
    8.26 +          Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
    8.27        | replace_types T = T;
    8.28  
    8.29      val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
     9.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Oct 20 23:25:04 2009 +0200
     9.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Oct 21 00:36:12 2009 +0200
     9.3 @@ -173,7 +173,7 @@
     9.4                   [Pretty.block [str "(case", Pretty.brk 1,
     9.5                     str "i", Pretty.brk 1, str "of",
     9.6                     Pretty.brk 1, str "0 =>", Pretty.brk 1,
     9.7 -                   mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
     9.8 +                   mk_constr "0" true (cname, the (AList.lookup (op =) cs cname)),
     9.9                     Pretty.brk 1, str "| _ =>", Pretty.brk 1,
    9.10                     mk_choice cs1, str ")"]]
    9.11                 else [mk_choice cs2])) ::
    10.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Tue Oct 20 23:25:04 2009 +0200
    10.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Oct 21 00:36:12 2009 +0200
    10.3 @@ -136,7 +136,7 @@
    10.4      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    10.5      val ivs1 = map Var (filter_out (fn (_, T) =>
    10.6        tname_of (body_type T) mem ["set", "bool"]) ivs);
    10.7 -    val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
    10.8 +    val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    10.9  
   10.10      val prf = List.foldr forall_intr_prf
   10.11       (List.foldr (fn ((f, p), prf) =>
    11.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Oct 20 23:25:04 2009 +0200
    11.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Oct 21 00:36:12 2009 +0200
    11.3 @@ -505,8 +505,8 @@
    11.4    val (l,r) = Thm.dest_equals eq
    11.5    val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l))
    11.6    val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r))
    11.7 -  fun tabl c = valOf (Termtab.lookup ctabl (term_of c))
    11.8 -  fun tabr c = valOf (Termtab.lookup ctabr (term_of c))
    11.9 +  fun tabl c = the (Termtab.lookup ctabl (term_of c))
   11.10 +  fun tabr c = the (Termtab.lookup ctabr (term_of c))
   11.11    val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   11.12    val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   11.13    val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
   11.14 @@ -839,7 +839,7 @@
   11.15     val (v,th1) = 
   11.16     case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of
   11.17      SOME v => (v,th')
   11.18 -   | NONE => (valOf (find_first 
   11.19 +   | NONE => (the (find_first 
   11.20            (fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
   11.21     val th2 = transitive th1 
   11.22          (instantiate' []  [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v] 
   11.23 @@ -851,7 +851,7 @@
   11.24   let 
   11.25    val (vars,bod) = strip_exists tm
   11.26    val cjs = striplist (dest_binary @{cterm "op &"}) bod
   11.27 -  val th1 = (valOf (get_first (try (isolate_variable vars)) cjs) 
   11.28 +  val th1 = (the (get_first (try (isolate_variable vars)) cjs) 
   11.29               handle Option => raise CTERM ("unwind_polys_conv",[tm]))
   11.30    val eq = Thm.lhs_of th1
   11.31    val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
   11.32 @@ -906,7 +906,7 @@
   11.33   fun solve_idealism evs ps eqs =
   11.34    if null evs then [] else
   11.35    let 
   11.36 -   val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> valOf
   11.37 +   val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the
   11.38     val evs' = subtract op aconvc evs (map snd cfs)
   11.39     val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs)
   11.40    in cfs @ solve_idealism evs' ps eqs'
    12.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Tue Oct 20 23:25:04 2009 +0200
    12.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Oct 21 00:36:12 2009 +0200
    12.3 @@ -325,7 +325,7 @@
    12.4      let val tab = fold Inttab.update
    12.5            (ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
    12.6      in
    12.7 -      fn ct => valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
    12.8 +      fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
    12.9          handle Option =>
   12.10            (writeln ("noz: Theorems-Table contains no entry for " ^
   12.11                Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   12.12 @@ -416,7 +416,7 @@
   12.13     in equal_elim (Thm.symmetric th) TrueI end;
   12.14   val dvd =
   12.15     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   12.16 -     fn ct => valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
   12.17 +     fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
   12.18         handle Option =>
   12.19          (writeln ("dvd: Theorems-Table contains no entry for" ^
   12.20              Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
   12.21 @@ -483,13 +483,13 @@
   12.22          (map (fn eq =>
   12.23                  let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
   12.24                      val th = if term_of s = term_of t
   12.25 -                             then valOf(Termtab.lookup inStab (term_of s))
   12.26 +                             then the (Termtab.lookup inStab (term_of s))
   12.27                               else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
   12.28 -                                [eq, valOf(Termtab.lookup inStab (term_of s))]
   12.29 +                                [eq, the (Termtab.lookup inStab (term_of s))]
   12.30                   in (term_of t, th) end)
   12.31                    sths) Termtab.empty
   12.32          in
   12.33 -          fn ct => valOf (Termtab.lookup tab (term_of ct))
   12.34 +          fn ct => the (Termtab.lookup tab (term_of ct))
   12.35              handle Option =>
   12.36                (writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
   12.37                  raise Option)
    13.1 --- a/src/HOL/Tools/Qelim/langford.ML	Tue Oct 20 23:25:04 2009 +0200
    13.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Wed Oct 21 00:36:12 2009 +0200
    13.3 @@ -101,8 +101,8 @@
    13.4  fun conj_aci_rule eq = 
    13.5   let 
    13.6    val (l,r) = Thm.dest_equals eq
    13.7 -  fun tabl c = valOf (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
    13.8 -  fun tabr c = valOf (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
    13.9 +  fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
   13.10 +  fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
   13.11    val ll = Thm.dest_arg l
   13.12    val rr = Thm.dest_arg r
   13.13    
    14.1 --- a/src/HOL/Tools/TFL/rules.ML	Tue Oct 20 23:25:04 2009 +0200
    14.2 +++ b/src/HOL/Tools/TFL/rules.ML	Wed Oct 21 00:36:12 2009 +0200
    14.3 @@ -658,7 +658,7 @@
    14.4    in (ants,get_lhs eq)
    14.5    end;
    14.6  
    14.7 -fun restricted t = isSome (S.find_term
    14.8 +fun restricted t = is_some (S.find_term
    14.9                              (fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
   14.10                              t)
   14.11  
   14.12 @@ -784,7 +784,7 @@
   14.13                val dummy = print_cterm "func:" (cterm_of thy func)
   14.14                val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
   14.15                val dummy = tc_list := (TC :: !tc_list)
   14.16 -              val nestedp = isSome (S.find_term is_func TC)
   14.17 +              val nestedp = is_some (S.find_term is_func TC)
   14.18                val dummy = if nestedp then say "nested" else say "not_nested"
   14.19                val dummy = term_ref := ([func,TC]@(!term_ref))
   14.20                val th' = if nestedp then raise RULES_ERR "solver" "nested function"
    15.1 --- a/src/HOL/Tools/TFL/tfl.ML	Tue Oct 20 23:25:04 2009 +0200
    15.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Wed Oct 21 00:36:12 2009 +0200
    15.3 @@ -724,7 +724,7 @@
    15.4  in
    15.5  fun build_ih f P (pat,TCs) =
    15.6   let val globals = S.free_vars_lr pat
    15.7 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
    15.8 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
    15.9       fun dest_TC tm =
   15.10           let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   15.11               val (R,y,_) = S.dest_relation R_y_pat
   15.12 @@ -753,7 +753,7 @@
   15.13  fun build_ih f (P,SV) (pat,TCs) =
   15.14   let val pat_vars = S.free_vars_lr pat
   15.15       val globals = pat_vars@SV
   15.16 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
   15.17 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   15.18       fun dest_TC tm =
   15.19           let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
   15.20               val (R,y,_) = S.dest_relation R_y_pat
   15.21 @@ -786,7 +786,7 @@
   15.22   let val tych = Thry.typecheck thy
   15.23       val antc = tych(#ant(S.dest_imp tm))
   15.24       val thm' = R.SPEC_ALL thm
   15.25 -     fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
   15.26 +     fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
   15.27       fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
   15.28       fun mk_ih ((TC,locals),th2,nested) =
   15.29           R.GENL (map tych locals)
    16.1 --- a/src/HOL/Tools/cnf_funcs.ML	Tue Oct 20 23:25:04 2009 +0200
    16.2 +++ b/src/HOL/Tools/cnf_funcs.ML	Wed Oct 21 00:36:12 2009 +0200
    16.3 @@ -489,7 +489,7 @@
    16.4  				else
    16.5  					NONE
    16.6  		in
    16.7 -			Int.max (max, getOpt (idx, 0))
    16.8 +			Int.max (max, the_default 0 idx)
    16.9  		end) (OldTerm.term_frees simp) 0)
   16.10  	(* finally, convert to definitional CNF (this should preserve the simplification) *)
   16.11  	val cnfx_thm = make_cnfx_thm_from_nnf simp
    17.1 --- a/src/HOL/Tools/lin_arith.ML	Tue Oct 20 23:25:04 2009 +0200
    17.2 +++ b/src/HOL/Tools/lin_arith.ML	Wed Oct 21 00:36:12 2009 +0200
    17.3 @@ -672,7 +672,7 @@
    17.4        (case split_once_items ctxt subgoal of
    17.5          SOME new_subgoals => split_loop (new_subgoals @ subgoals)
    17.6        | NONE              => subgoal :: split_loop subgoals)
    17.7 -  fun is_relevant t  = isSome (decomp ctxt t)
    17.8 +  fun is_relevant t  = is_some (decomp ctxt t)
    17.9    (* filter_prems_tac is_relevant: *)
   17.10    val relevant_terms = filter_prems_tac_items is_relevant terms
   17.11    (* split_tac, NNF normalization: *)
   17.12 @@ -746,7 +746,7 @@
   17.13  fun pre_tac ctxt i =
   17.14  let
   17.15    val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
   17.16 -  fun is_relevant t = isSome (decomp ctxt t)
   17.17 +  fun is_relevant t = is_some (decomp ctxt t)
   17.18  in
   17.19    DETERM (
   17.20      TRY (filter_prems_tac is_relevant i)
   17.21 @@ -878,7 +878,7 @@
   17.22  local
   17.23  
   17.24  fun raw_tac ctxt ex =
   17.25 -  (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
   17.26 +  (* FIXME: K true should be replaced by a sensible test (perhaps "is_some o
   17.27       decomp sg"? -- but note that the test is applied to terms already before
   17.28       they are split/normalized) to speed things up in case there are lots of
   17.29       irrelevant terms involved; elimination of min/max can be optimized:
    18.1 --- a/src/HOL/Tools/metis_tools.ML	Tue Oct 20 23:25:04 2009 +0200
    18.2 +++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 21 00:36:12 2009 +0200
    18.3 @@ -123,7 +123,7 @@
    18.4    | metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
    18.5  
    18.6  fun default_sort _ (TVar _) = false
    18.7 -  | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), []));
    18.8 +  | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
    18.9  
   18.10  fun metis_of_tfree tf =
   18.11    Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
   18.12 @@ -204,7 +204,7 @@
   18.13  (*include the default sort, if available*)
   18.14  fun mk_tfree ctxt w =
   18.15    let val ww = "'" ^ w
   18.16 -  in  TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS))  end;
   18.17 +  in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   18.18  
   18.19  (*Remove the "apply" operator from an HO term*)
   18.20  fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   18.21 @@ -342,7 +342,7 @@
   18.22     trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
   18.23  
   18.24  fun lookth thpairs (fth : Metis.Thm.thm) =
   18.25 -  valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   18.26 +  the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
   18.27    handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
   18.28  
   18.29  fun is_TrueI th = Thm.eq_thm(TrueI,th);
   18.30 @@ -372,7 +372,7 @@
   18.31    let val thy = ProofContext.theory_of ctxt
   18.32        val i_th   = lookth thpairs th
   18.33        val i_th_vars = Term.add_vars (prop_of i_th) []
   18.34 -      fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
   18.35 +      fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
   18.36        fun subst_translation (x,y) =
   18.37              let val v = find_var x
   18.38                  val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
    19.1 --- a/src/HOL/Tools/refute.ML	Tue Oct 20 23:25:04 2009 +0200
    19.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 21 00:36:12 2009 +0200
    19.3 @@ -1081,7 +1081,7 @@
    19.4        | next max len sum (x1::x2::xs) =
    19.5        if x1>0 andalso (x2<max orelse max<0) then
    19.6          (* we can shift *)
    19.7 -        SOME (valOf (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
    19.8 +        SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
    19.9        else
   19.10          (* continue search *)
   19.11          next max (len+1) (sum+x1) (x2::xs)
    20.1 --- a/src/HOL/Tools/res_atp.ML	Tue Oct 20 23:25:04 2009 +0200
    20.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 21 00:36:12 2009 +0200
    20.3 @@ -352,7 +352,7 @@
    20.4    boost an ATP's performance (for some reason)*)
    20.5  fun subtract_cls c_clauses ax_clauses =
    20.6    let val ht = mk_clause_table 2200
    20.7 -      fun known x = isSome (Polyhash.peek ht x)
    20.8 +      fun known x = is_some (Polyhash.peek ht x)
    20.9    in
   20.10        app (ignore o Polyhash.peekInsert ht) ax_clauses;
   20.11        filter (not o known) c_clauses
   20.12 @@ -391,7 +391,7 @@
   20.13  fun name_thm_pairs ctxt =
   20.14    let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   20.15        val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   20.16 -      fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   20.17 +      fun blacklisted x = run_blacklist_filter andalso is_some (Polyhash.peek ht x)
   20.18    in
   20.19        app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   20.20        filter (not o blacklisted o #2)
    21.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 23:25:04 2009 +0200
    21.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 00:36:12 2009 +0200
    21.3 @@ -69,12 +69,13 @@
    21.4    use of the "apply" operator. Use of hBOOL is also minimized.*)
    21.5  val minimize_applies = true;
    21.6  
    21.7 -fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
    21.8 +fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
    21.9  
   21.10  (*True if the constant ever appears outside of the top-level position in literals.
   21.11    If false, the constant always receives all of its arguments and is used as a predicate.*)
   21.12 -fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
   21.13 -                    getOpt (Symtab.lookup const_needs_hBOOL c, false);
   21.14 +fun needs_hBOOL const_needs_hBOOL c =
   21.15 +  not minimize_applies orelse
   21.16 +    the_default false (Symtab.lookup const_needs_hBOOL c);
   21.17  
   21.18  
   21.19  (******************************************************)
   21.20 @@ -412,7 +413,7 @@
   21.21          val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
   21.22          val ct0 = List.foldl count_clause init_counters conjectures
   21.23          val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
   21.24 -        fun needed c = valOf (Symtab.lookup ct c) > 0
   21.25 +        fun needed c = the (Symtab.lookup ct c) > 0
   21.26          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
   21.27                   then cnf_helper_thms thy [comb_I,comb_K]
   21.28                   else []
    22.1 --- a/src/HOL/Tools/res_reconstruct.ML	Tue Oct 20 23:25:04 2009 +0200
    22.2 +++ b/src/HOL/Tools/res_reconstruct.ML	Wed Oct 21 00:36:12 2009 +0200
    22.3 @@ -64,7 +64,7 @@
    22.4  
    22.5  (*Integer constants, typically proof line numbers*)
    22.6  fun is_digit s = Char.isDigit (String.sub(s,0));
    22.7 -val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
    22.8 +val integer = Scan.many1 is_digit >> (the o Int.fromString o implode);
    22.9  
   22.10  (*Generalized FO terms, which include filenames, numbers, etc.*)
   22.11  fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
   22.12 @@ -225,8 +225,8 @@
   22.13  (*Update TVars/TFrees with detected sort constraints.*)
   22.14  fun fix_sorts vt =
   22.15    let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
   22.16 -        | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s))
   22.17 -        | tysubst (TFree (x, s)) = TFree (x, getOpt (Vartab.lookup vt (x,~1), s))
   22.18 +        | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
   22.19 +        | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
   22.20        fun tmsubst (Const (a, T)) = Const (a, tysubst T)
   22.21          | tmsubst (Free (a, T)) = Free (a, tysubst T)
   22.22          | tmsubst (Var (xi, T)) = Var (xi, tysubst T)
    23.1 --- a/src/HOL/Tools/sat_funcs.ML	Tue Oct 20 23:25:04 2009 +0200
    23.2 +++ b/src/HOL/Tools/sat_funcs.ML	Wed Oct 21 00:36:12 2009 +0200
    23.3 @@ -218,9 +218,9 @@
    23.4  	fun index_of_literal chyp = (
    23.5  		case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
    23.6  		  (Const ("Not", _) $ atom) =>
    23.7 -			SOME (~(valOf (Termtab.lookup atom_table atom)))
    23.8 +			SOME (~ (the (Termtab.lookup atom_table atom)))
    23.9  		| atom =>
   23.10 -			SOME (valOf (Termtab.lookup atom_table atom))
   23.11 +			SOME (the (Termtab.lookup atom_table atom))
   23.12  	) handle TERM _ => NONE;  (* 'chyp' is not a literal *)
   23.13  
   23.14  	(* int -> Thm.thm * (int * Thm.cterm) list *)
   23.15 @@ -244,7 +244,7 @@
   23.16  			(* prove the clause, using information from 'clause_table' *)
   23.17  			let
   23.18  				val _      = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
   23.19 -				val ids    = valOf (Inttab.lookup clause_table id)
   23.20 +				val ids    = the (Inttab.lookup clause_table id)
   23.21  				val clause = resolve_raw_clauses (map prove_clause ids)
   23.22  				val _      = Array.update (clauses, id, RAW_CLAUSE clause)
   23.23  				val _      = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
   23.24 @@ -367,7 +367,7 @@
   23.25  				(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
   23.26  				val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
   23.27  				(* initialize the clause array with the given clauses *)
   23.28 -				val max_idx    = valOf (Inttab.max_key clause_table)
   23.29 +				val max_idx    = the (Inttab.max_key clause_table)
   23.30  				val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
   23.31  				val _          = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
   23.32  				(* replay the proof to derive the empty clause *)
    24.1 --- a/src/HOL/Tools/sat_solver.ML	Tue Oct 20 23:25:04 2009 +0200
    24.2 +++ b/src/HOL/Tools/sat_solver.ML	Wed Oct 21 00:36:12 2009 +0200
    24.3 @@ -502,7 +502,7 @@
    24.4          | False => NONE
    24.5          | _     =>
    24.6            let
    24.7 -            val x = valOf (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
    24.8 +            val x = the (fresh_var xs')  (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
    24.9            in
   24.10              case dpll (x::xs') fm' of  (* passing fm' rather than fm should save some simplification work *)
   24.11                SOME xs'' => SOME xs''
   24.12 @@ -893,7 +893,7 @@
   24.13                (* for its literals to obtain the empty clause                *)
   24.14                val vids         = map (fn l => l div 2) ls
   24.15                val rs           = cid :: map (fn v => !clause_offset + v) vids
   24.16 -              val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
   24.17 +              val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1
   24.18              in
   24.19                (* update clause table and conflict id *)
   24.20                clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
    25.1 --- a/src/Pure/ProofGeneral/pgip_output.ML	Tue Oct 20 23:25:04 2009 +0200
    25.2 +++ b/src/Pure/ProofGeneral/pgip_output.ML	Wed Oct 21 00:36:12 2009 +0200
    25.3 @@ -219,8 +219,8 @@
    25.4          fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
    25.5      in
    25.6          XML.Elem ("setrefs",
    25.7 -                  (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @ 
    25.8 -                  (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
    25.9 +                  (the_default [] (Option.map attrs_of_pgipurl url)) @ 
   25.10 +                  (the_default [] (Option.map attrs_of_objtype objtype)) @
   25.11                    (opt_attr "thyname" thyname) @
   25.12                    (opt_attr "name" name),
   25.13                    (map idtable_to_xml idtables) @ 
    26.1 --- a/src/Pure/ProofGeneral/pgml.ML	Tue Oct 20 23:25:04 2009 +0200
    26.2 +++ b/src/Pure/ProofGeneral/pgml.ML	Wed Oct 21 00:36:12 2009 +0200
    26.3 @@ -155,6 +155,6 @@
    26.4          XML.Elem("pgml",
    26.5                   opt_attr "version" version @
    26.6                   opt_attr "systemid" systemid @
    26.7 -                 Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
    26.8 +                 the_default [] (Option.map PgipTypes.attrs_of_displayarea area),
    26.9                   map pgmlterm_to_xml content)
   26.10  end