--- a/src/HOL/Import/proof_kernel.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Import/proof_kernel.ML Wed Oct 21 00:36:12 2009 +0200
@@ -583,7 +583,7 @@
fun input_types thyname (Elem("tylist",[("i",i)],xtys)) =
let
- val types = Array.array(valOf (Int.fromString i),XMLty (Elem("",[],[])))
+ val types = Array.array(the (Int.fromString i),XMLty (Elem("",[],[])))
fun IT _ [] = ()
| IT n (xty::xtys) =
(Array.update(types,n,XMLty xty);
@@ -650,7 +650,7 @@
fun input_terms thyname types (Elem("tmlist",[("i",i)],xtms)) =
let
- val terms = Array.array(valOf(Int.fromString i),XMLtm (Elem("",[],[])))
+ val terms = Array.array(the (Int.fromString i), XMLtm (Elem("",[],[])))
fun IT _ [] = ()
| IT n (xtm::xtms) =
@@ -1239,7 +1239,7 @@
val (newstr,u) = pairself Substring.string (Substring.splitr (fn c => c = #"_") f)
in
if not (idx = "") andalso u = "_"
- then SOME (newstr,valOf(Int.fromString idx))
+ then SOME (newstr, the (Int.fromString idx))
else NONE
end
handle _ => NONE (* FIXME avoid handle _ *)
@@ -1914,7 +1914,7 @@
fun new_definition thyname constname rhs thy =
let
val constname = rename_const thyname thy constname
- val redeclared = isSome (Sign.const_type thy (Sign.intern_const thy constname));
+ val redeclared = is_some (Sign.const_type thy (Sign.intern_const thy constname));
val _ = warning ("Introducing constant " ^ constname)
val (thmname,thy) = get_defname thyname constname thy
val (info,rhs') = disamb_term rhs
--- a/src/HOL/Import/replay.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Import/replay.ML Wed Oct 21 00:36:12 2009 +0200
@@ -291,7 +291,7 @@
fun get_facts facts =
case TextIO.inputLine is of
NONE => (case facts of
- i::facts => (valOf (Int.fromString i),map P.protect_factname (rev facts))
+ i::facts => (the (Int.fromString i),map P.protect_factname (rev facts))
| _ => raise ERR "replay_thm" "Bad facts.lst file")
| SOME fact => get_facts ((String.substring(fact,0,String.size fact -1 ))::facts)
in
--- a/src/HOL/Library/Numeral_Type.thy Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy Wed Oct 21 00:36:12 2009 +0200
@@ -408,7 +408,7 @@
in bin_of n end;
fun numeral_tr (*"_NumeralType"*) [Const (str, _)] =
- mk_bintype (valOf (Int.fromString str))
+ mk_bintype (the (Int.fromString str))
| numeral_tr (*"_NumeralType"*) ts = raise TERM ("numeral_tr", ts);
in [("_NumeralType", numeral_tr)] end;
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Wed Oct 21 00:36:12 2009 +0200
@@ -520,7 +520,7 @@
fun rat_of_quotient (a,b) = if b = 0 then rat_0 else Rat.rat_of_quotient (a,b);
fun rat_of_string s =
let val n = index_char s #"/" 0 in
- if n = ~1 then s |> Int.fromString |> valOf |> Rat.rat_of_int
+ if n = ~1 then s |> Int.fromString |> the |> Rat.rat_of_int
else
let val SOME numer = Int.fromString(String.substring(s,0,n))
val SOME den = Int.fromString (String.substring(s,n+1,String.size s - n - 1))
@@ -1193,7 +1193,7 @@
fun real_nonlinear_prover proof_method ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
@@ -1308,7 +1308,7 @@
fun real_nonlinear_subst_prover prover ctxt =
let
val {add,mul,neg,pow,sub,main} = Normalizer.semiring_normalizers_ord_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
val (real_poly_add_conv,real_poly_mul_conv,real_poly_neg_conv,
--- a/src/HOL/Library/normarith.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Library/normarith.ML Wed Oct 21 00:36:12 2009 +0200
@@ -167,7 +167,7 @@
(* FIXME : Should be computed statically!! *)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
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)))
end;
@@ -278,7 +278,7 @@
(* FIXME: Should be computed statically!!*)
val real_poly_conv =
Normalizer.semiring_normalize_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
val sources = map (Thm.dest_arg o Thm.dest_arg1 o concl) nubs
val rawdests = fold_rev (find_normedterms o Thm.dest_arg o concl) (ges @ gts) []
val _ = if not (forall fst rawdests) then error "real_vector_combo_prover: Sanity check"
@@ -384,7 +384,7 @@
let
val real_poly_neg_conv = #neg
(Normalizer.semiring_normalizers_ord_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"})) simple_cterm_ord)
val (th1,th2) = conj_pair(rawrule th)
in th1::fconv_rule (arg_conv (arg_conv real_poly_neg_conv)) th2::acc
end
--- a/src/HOL/Library/positivstellensatz.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Wed Oct 21 00:36:12 2009 +0200
@@ -43,7 +43,7 @@
in Tab.fold h a b end;
fun choose f = case Tab.min_key f of
- SOME k => (k,valOf (Tab.lookup f k))
+ SOME k => (k, the (Tab.lookup f k))
| NONE => error "FuncFun.choose : Completely empty function"
fun onefunc kv = update kv empty
@@ -743,7 +743,7 @@
fun simple_cterm_ord t u = TermOrd.term_ord (term_of t, term_of u) = LESS
val {add,mul,neg,pow,sub,main} =
Normalizer.semiring_normalizers_ord_wrapper ctxt
- (valOf (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
+ (the (NormalizerData.match ctxt @{cterm "(0::real) + 1"}))
simple_cterm_ord
in gen_real_arith ctxt
(cterm_of_rat, field_comp_conv, field_comp_conv,field_comp_conv,
--- a/src/HOL/Modelcheck/MuckeSyn.thy Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy Wed Oct 21 00:36:12 2009 +0200
@@ -123,8 +123,8 @@
REPEAT (resolve_tac prems 1)]);
val sig_move_thm = Thm.theory_of_thm move_thm;
- val bCterm = cterm_of sig_move_thm (valOf (search_var "b" (concl_of move_thm)));
- val aCterm = cterm_of sig_move_thm (valOf (search_var "a" (hd(prems_of move_thm))));
+ val bCterm = cterm_of sig_move_thm (the (search_var "b" (concl_of move_thm)));
+ val aCterm = cterm_of sig_move_thm (the (search_var "a" (hd(prems_of move_thm))));
in
--- a/src/HOL/Nominal/nominal_datatype.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Oct 21 00:36:12 2009 +0200
@@ -50,7 +50,7 @@
fun dt_cases (descr: descr) (_, args, constrs) =
let
- fun the_bname i = Long_Name.base_name (#1 (valOf (AList.lookup (op =) descr i)));
+ fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
val bnames = map the_bname (distinct op = (maps dt_recs args));
in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
@@ -58,7 +58,7 @@
fun induct_cases descr =
DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
-fun exhaust_cases descr i = dt_cases descr (valOf (AList.lookup (op =) descr i));
+fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
in
@@ -233,7 +233,7 @@
fun replace_types (Type ("Nominal.ABS", [T, U])) =
Type ("fun", [T, Type ("Nominal.noption", [replace_types U])])
| replace_types (Type (s, Ts)) =
- Type (getOpt (AList.lookup op = ps s, s), map replace_types Ts)
+ Type (the_default s (AList.lookup op = ps s), map replace_types Ts)
| replace_types T = T;
val dts'' = map (fn (tvs, tname, mx, constrs) => (tvs, Binding.name (tname ^ "_Rep"), NoSyn,
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Oct 21 00:36:12 2009 +0200
@@ -173,7 +173,7 @@
[Pretty.block [str "(case", Pretty.brk 1,
str "i", Pretty.brk 1, str "of",
Pretty.brk 1, str "0 =>", Pretty.brk 1,
- mk_constr "0" true (cname, valOf (AList.lookup (op =) cs cname)),
+ mk_constr "0" true (cname, the (AList.lookup (op =) cs cname)),
Pretty.brk 1, str "| _ =>", Pretty.brk 1,
mk_choice cs1, str ")"]]
else [mk_choice cs2])) ::
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Oct 21 00:36:12 2009 +0200
@@ -136,7 +136,7 @@
val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
val ivs1 = map Var (filter_out (fn (_, T) =>
tname_of (body_type T) mem ["set", "bool"]) ivs);
- val ivs2 = map (fn (ixn, _) => Var (ixn, valOf (AList.lookup (op =) rvs ixn))) ivs;
+ val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
val prf = List.foldr forall_intr_prf
(List.foldr (fn ((f, p), prf) =>
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML Wed Oct 21 00:36:12 2009 +0200
@@ -505,8 +505,8 @@
val (l,r) = Thm.dest_equals eq
val ctabl = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} l))
val ctabr = mk_conj_tab (assume (Thm.capply @{cterm Trueprop} r))
- fun tabl c = valOf (Termtab.lookup ctabl (term_of c))
- fun tabr c = valOf (Termtab.lookup ctabr (term_of c))
+ fun tabl c = the (Termtab.lookup ctabl (term_of c))
+ fun tabr c = the (Termtab.lookup ctabr (term_of c))
val thl = prove_conj tabl (conjuncts r) |> implies_intr_hyps
val thr = prove_conj tabr (conjuncts l) |> implies_intr_hyps
val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}
@@ -839,7 +839,7 @@
val (v,th1) =
case find_first(fn v=> is_defined v (Thm.dest_arg1 (Thm.rhs_of th))) vars of
SOME v => (v,th')
- | NONE => (valOf (find_first
+ | NONE => (the (find_first
(fn v => is_defined v (Thm.dest_arg1 (Thm.rhs_of th'))) vars) ,th)
val th2 = transitive th1
(instantiate' [] [(SOME o Thm.dest_arg1 o Thm.rhs_of) th1, SOME v]
@@ -851,7 +851,7 @@
let
val (vars,bod) = strip_exists tm
val cjs = striplist (dest_binary @{cterm "op &"}) bod
- val th1 = (valOf (get_first (try (isolate_variable vars)) cjs)
+ val th1 = (the (get_first (try (isolate_variable vars)) cjs)
handle Option => raise CTERM ("unwind_polys_conv",[tm]))
val eq = Thm.lhs_of th1
val bod' = list_mk_binop @{cterm "op &"} (eq::(remove op aconvc eq cjs))
@@ -906,7 +906,7 @@
fun solve_idealism evs ps eqs =
if null evs then [] else
let
- val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> valOf
+ val (eq,cfs) = get_first (try (isolate_variables evs ps)) eqs |> the
val evs' = subtract op aconvc evs (map snd cfs)
val eqs' = map (subst_in_poly cfs) (remove op aconvc eq eqs)
in cfs @ solve_idealism evs' ps eqs'
--- a/src/HOL/Tools/Qelim/cooper.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 21 00:36:12 2009 +0200
@@ -325,7 +325,7 @@
let val tab = fold Inttab.update
(ds ~~ (map (fn x => nzprop (l div x)) ds)) Inttab.empty
in
- fn ct => valOf (Inttab.lookup tab (ct |> term_of |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (ct |> term_of |> dest_numeral))
handle Option =>
(writeln ("noz: Theorems-Table contains no entry for " ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -416,7 +416,7 @@
in equal_elim (Thm.symmetric th) TrueI end;
val dvd =
let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
- fn ct => valOf (Inttab.lookup tab (term_of ct |> dest_numeral))
+ fn ct => the (Inttab.lookup tab (term_of ct |> dest_numeral))
handle Option =>
(writeln ("dvd: Theorems-Table contains no entry for" ^
Syntax.string_of_term ctxt (Thm.term_of ct)); raise Option)
@@ -483,13 +483,13 @@
(map (fn eq =>
let val (s,t) = cprop_of eq |> Thm.dest_arg |> Thm.dest_binop
val th = if term_of s = term_of t
- then valOf(Termtab.lookup inStab (term_of s))
+ then the (Termtab.lookup inStab (term_of s))
else FWD (instantiate' [] [SOME s, SOME t] eqelem_th)
- [eq, valOf(Termtab.lookup inStab (term_of s))]
+ [eq, the (Termtab.lookup inStab (term_of s))]
in (term_of t, th) end)
sths) Termtab.empty
in
- fn ct => valOf (Termtab.lookup tab (term_of ct))
+ fn ct => the (Termtab.lookup tab (term_of ct))
handle Option =>
(writeln ("inS: No theorem for " ^ Syntax.string_of_term ctxt (Thm.term_of ct));
raise Option)
--- a/src/HOL/Tools/Qelim/langford.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/Qelim/langford.ML Wed Oct 21 00:36:12 2009 +0200
@@ -101,8 +101,8 @@
fun conj_aci_rule eq =
let
val (l,r) = Thm.dest_equals eq
- fun tabl c = valOf (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
- fun tabr c = valOf (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
+ fun tabl c = the (Termtab.lookup (mk_conj_tab (assume l)) (term_of c))
+ fun tabr c = the (Termtab.lookup (mk_conj_tab (assume r)) (term_of c))
val ll = Thm.dest_arg l
val rr = Thm.dest_arg r
--- a/src/HOL/Tools/TFL/rules.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Wed Oct 21 00:36:12 2009 +0200
@@ -658,7 +658,7 @@
in (ants,get_lhs eq)
end;
-fun restricted t = isSome (S.find_term
+fun restricted t = is_some (S.find_term
(fn (Const(@{const_name Recdef.cut},_)) =>true | _ => false)
t)
@@ -784,7 +784,7 @@
val dummy = print_cterm "func:" (cterm_of thy func)
val dummy = print_cterm "TC:" (cterm_of thy (HOLogic.mk_Trueprop TC))
val dummy = tc_list := (TC :: !tc_list)
- val nestedp = isSome (S.find_term is_func TC)
+ val nestedp = is_some (S.find_term is_func TC)
val dummy = if nestedp then say "nested" else say "not_nested"
val dummy = term_ref := ([func,TC]@(!term_ref))
val th' = if nestedp then raise RULES_ERR "solver" "nested function"
--- a/src/HOL/Tools/TFL/tfl.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/TFL/tfl.ML Wed Oct 21 00:36:12 2009 +0200
@@ -724,7 +724,7 @@
in
fun build_ih f P (pat,TCs) =
let val globals = S.free_vars_lr pat
- fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
val (R,y,_) = S.dest_relation R_y_pat
@@ -753,7 +753,7 @@
fun build_ih f (P,SV) (pat,TCs) =
let val pat_vars = S.free_vars_lr pat
val globals = pat_vars@SV
- fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
fun dest_TC tm =
let val (cntxt,R_y_pat) = S.strip_imp(#2(S.strip_forall tm))
val (R,y,_) = S.dest_relation R_y_pat
@@ -786,7 +786,7 @@
let val tych = Thry.typecheck thy
val antc = tych(#ant(S.dest_imp tm))
val thm' = R.SPEC_ALL thm
- fun nested tm = isSome (S.find_term (curry (op aconv) f) tm)
+ fun nested tm = is_some (S.find_term (curry (op aconv) f) tm)
fun get_cntxt TC = tych(#ant(S.dest_imp(#2(S.strip_forall(concl TC)))))
fun mk_ih ((TC,locals),th2,nested) =
R.GENL (map tych locals)
--- a/src/HOL/Tools/cnf_funcs.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/cnf_funcs.ML Wed Oct 21 00:36:12 2009 +0200
@@ -489,7 +489,7 @@
else
NONE
in
- Int.max (max, getOpt (idx, 0))
+ Int.max (max, the_default 0 idx)
end) (OldTerm.term_frees simp) 0)
(* finally, convert to definitional CNF (this should preserve the simplification) *)
val cnfx_thm = make_cnfx_thm_from_nnf simp
--- a/src/HOL/Tools/lin_arith.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/lin_arith.ML Wed Oct 21 00:36:12 2009 +0200
@@ -672,7 +672,7 @@
(case split_once_items ctxt subgoal of
SOME new_subgoals => split_loop (new_subgoals @ subgoals)
| NONE => subgoal :: split_loop subgoals)
- fun is_relevant t = isSome (decomp ctxt t)
+ fun is_relevant t = is_some (decomp ctxt t)
(* filter_prems_tac is_relevant: *)
val relevant_terms = filter_prems_tac_items is_relevant terms
(* split_tac, NNF normalization: *)
@@ -746,7 +746,7 @@
fun pre_tac ctxt i =
let
val split_thms = filter is_split_thm (#splits (get_arith_data ctxt))
- fun is_relevant t = isSome (decomp ctxt t)
+ fun is_relevant t = is_some (decomp ctxt t)
in
DETERM (
TRY (filter_prems_tac is_relevant i)
@@ -878,7 +878,7 @@
local
fun raw_tac ctxt ex =
- (* FIXME: K true should be replaced by a sensible test (perhaps "isSome o
+ (* FIXME: K true should be replaced by a sensible test (perhaps "is_some o
decomp sg"? -- but note that the test is applied to terms already before
they are split/normalized) to speed things up in case there are lots of
irrelevant terms involved; elimination of min/max can be optimized:
--- a/src/HOL/Tools/metis_tools.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/metis_tools.ML Wed Oct 21 00:36:12 2009 +0200
@@ -123,7 +123,7 @@
| metis_of_typeLit pos (ResClause.LTFree (s,x)) = metis_lit pos s [Metis.Term.Fn(x,[])];
fun default_sort _ (TVar _) = false
- | default_sort ctxt (TFree (x, s)) = (s = Option.getOpt (Variable.def_sort ctxt (x, ~1), []));
+ | default_sort ctxt (TFree (x, s)) = (s = the_default [] (Variable.def_sort ctxt (x, ~1)));
fun metis_of_tfree tf =
Metis.Thm.axiom (Metis.LiteralSet.singleton (metis_of_typeLit true tf));
@@ -204,7 +204,7 @@
(*include the default sort, if available*)
fun mk_tfree ctxt w =
let val ww = "'" ^ w
- in TFree(ww, getOpt (Variable.def_sort ctxt (ww,~1), HOLogic.typeS)) end;
+ in TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1))) end;
(*Remove the "apply" operator from an HO term*)
fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
@@ -342,7 +342,7 @@
trace_msg (fn () => "Isabelle: " ^ Display.string_of_thm_without_context th));
fun lookth thpairs (fth : Metis.Thm.thm) =
- valOf (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
+ the (AList.lookup (uncurry Metis.Thm.equal) thpairs fth)
handle Option => error ("Failed to find a Metis theorem " ^ Metis.Thm.toString fth);
fun is_TrueI th = Thm.eq_thm(TrueI,th);
@@ -372,7 +372,7 @@
let val thy = ProofContext.theory_of ctxt
val i_th = lookth thpairs th
val i_th_vars = Term.add_vars (prop_of i_th) []
- fun find_var x = valOf (List.find (fn ((a,_),_) => a=x) i_th_vars)
+ fun find_var x = the (List.find (fn ((a,_),_) => a=x) i_th_vars)
fun subst_translation (x,y) =
let val v = find_var x
val t = fol_term_to_hol ctxt mode y (*we call infer_types below*)
--- a/src/HOL/Tools/refute.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/refute.ML Wed Oct 21 00:36:12 2009 +0200
@@ -1081,7 +1081,7 @@
| next max len sum (x1::x2::xs) =
if x1>0 andalso (x2<max orelse max<0) then
(* we can shift *)
- SOME (valOf (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
+ SOME (the (make_first max (len+1) (sum+x1-1)) @ (x2+1) :: xs)
else
(* continue search *)
next max (len+1) (sum+x1) (x2::xs)
--- a/src/HOL/Tools/res_atp.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Oct 21 00:36:12 2009 +0200
@@ -352,7 +352,7 @@
boost an ATP's performance (for some reason)*)
fun subtract_cls c_clauses ax_clauses =
let val ht = mk_clause_table 2200
- fun known x = isSome (Polyhash.peek ht x)
+ fun known x = is_some (Polyhash.peek ht x)
in
app (ignore o Polyhash.peekInsert ht) ax_clauses;
filter (not o known) c_clauses
@@ -391,7 +391,7 @@
fun name_thm_pairs ctxt =
let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
val ht = mk_clause_table 900 (*ht for blacklisted theorems*)
- fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x)
+ fun blacklisted x = run_blacklist_filter andalso is_some (Polyhash.peek ht x)
in
app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
filter (not o blacklisted o #2)
--- a/src/HOL/Tools/res_hol_clause.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML Wed Oct 21 00:36:12 2009 +0200
@@ -69,12 +69,13 @@
use of the "apply" operator. Use of hBOOL is also minimized.*)
val minimize_applies = true;
-fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
+fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
(*True if the constant ever appears outside of the top-level position in literals.
If false, the constant always receives all of its arguments and is used as a predicate.*)
-fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
- getOpt (Symtab.lookup const_needs_hBOOL c, false);
+fun needs_hBOOL const_needs_hBOOL c =
+ not minimize_applies orelse
+ the_default false (Symtab.lookup const_needs_hBOOL c);
(******************************************************)
@@ -412,7 +413,7 @@
val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
val ct0 = List.foldl count_clause init_counters conjectures
val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
- fun needed c = valOf (Symtab.lookup ct c) > 0
+ fun needed c = the (Symtab.lookup ct c) > 0
val IK = if needed "c_COMBI" orelse needed "c_COMBK"
then cnf_helper_thms thy [comb_I,comb_K]
else []
--- a/src/HOL/Tools/res_reconstruct.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Oct 21 00:36:12 2009 +0200
@@ -64,7 +64,7 @@
(*Integer constants, typically proof line numbers*)
fun is_digit s = Char.isDigit (String.sub(s,0));
-val integer = Scan.many1 is_digit >> (valOf o Int.fromString o implode);
+val integer = Scan.many1 is_digit >> (the o Int.fromString o implode);
(*Generalized FO terms, which include filenames, numbers, etc.*)
fun termlist x = (term ::: Scan.repeat ($$"," |-- term)) x
@@ -225,8 +225,8 @@
(*Update TVars/TFrees with detected sort constraints.*)
fun fix_sorts vt =
let fun tysubst (Type (a, Ts)) = Type (a, map tysubst Ts)
- | tysubst (TVar (xi, s)) = TVar (xi, getOpt (Vartab.lookup vt xi, s))
- | tysubst (TFree (x, s)) = TFree (x, getOpt (Vartab.lookup vt (x,~1), s))
+ | tysubst (TVar (xi, s)) = TVar (xi, the_default s (Vartab.lookup vt xi))
+ | tysubst (TFree (x, s)) = TFree (x, the_default s (Vartab.lookup vt (x, ~1)))
fun tmsubst (Const (a, T)) = Const (a, tysubst T)
| tmsubst (Free (a, T)) = Free (a, tysubst T)
| tmsubst (Var (xi, T)) = Var (xi, tysubst T)
--- a/src/HOL/Tools/sat_funcs.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML Wed Oct 21 00:36:12 2009 +0200
@@ -218,9 +218,9 @@
fun index_of_literal chyp = (
case (HOLogic.dest_Trueprop o Thm.term_of) chyp of
(Const ("Not", _) $ atom) =>
- SOME (~(valOf (Termtab.lookup atom_table atom)))
+ SOME (~ (the (Termtab.lookup atom_table atom)))
| atom =>
- SOME (valOf (Termtab.lookup atom_table atom))
+ SOME (the (Termtab.lookup atom_table atom))
) handle TERM _ => NONE; (* 'chyp' is not a literal *)
(* int -> Thm.thm * (int * Thm.cterm) list *)
@@ -244,7 +244,7 @@
(* prove the clause, using information from 'clause_table' *)
let
val _ = if !trace_sat then tracing ("Proving clause #" ^ string_of_int id ^ " ...") else ()
- val ids = valOf (Inttab.lookup clause_table id)
+ val ids = the (Inttab.lookup clause_table id)
val clause = resolve_raw_clauses (map prove_clause ids)
val _ = Array.update (clauses, id, RAW_CLAUSE clause)
val _ = if !trace_sat then tracing ("Replay chain successful; clause stored at #" ^ string_of_int id) else ()
@@ -367,7 +367,7 @@
(* [[c_1 && ... && c_n] |- c_1, ..., [c_1 && ... && c_n] |- c_n] *)
val cnf_clauses = Conjunction.elim_balanced (length sorted_clauses) cnf_thm
(* initialize the clause array with the given clauses *)
- val max_idx = valOf (Inttab.max_key clause_table)
+ val max_idx = the (Inttab.max_key clause_table)
val clause_arr = Array.array (max_idx + 1, NO_CLAUSE)
val _ = fold (fn thm => fn idx => (Array.update (clause_arr, idx, ORIG_CLAUSE thm); idx+1)) cnf_clauses 0
(* replay the proof to derive the empty clause *)
--- a/src/HOL/Tools/sat_solver.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/HOL/Tools/sat_solver.ML Wed Oct 21 00:36:12 2009 +0200
@@ -502,7 +502,7 @@
| False => NONE
| _ =>
let
- val x = valOf (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
+ val x = the (fresh_var xs') (* a fresh variable must exist since 'fm' did not evaluate to 'True'/'False' *)
in
case dpll (x::xs') fm' of (* passing fm' rather than fm should save some simplification work *)
SOME xs'' => SOME xs''
@@ -893,7 +893,7 @@
(* for its literals to obtain the empty clause *)
val vids = map (fn l => l div 2) ls
val rs = cid :: map (fn v => !clause_offset + v) vids
- val new_empty_id = getOpt (Inttab.max_key (!clause_table), !clause_offset) + 1
+ val new_empty_id = the_default (!clause_offset) (Inttab.max_key (!clause_table)) + 1
in
(* update clause table and conflict id *)
clause_table := Inttab.update_new (new_empty_id, rs) (!clause_table)
--- a/src/Pure/ProofGeneral/pgip_output.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/Pure/ProofGeneral/pgip_output.ML Wed Oct 21 00:36:12 2009 +0200
@@ -219,8 +219,8 @@
fun fileurl_to_xml url = XML.Elem ("fileurl", attrs_of_pgipurl url, [])
in
XML.Elem ("setrefs",
- (Option.getOpt (Option.map attrs_of_pgipurl url,[])) @
- (Option.getOpt (Option.map attrs_of_objtype objtype,[])) @
+ (the_default [] (Option.map attrs_of_pgipurl url)) @
+ (the_default [] (Option.map attrs_of_objtype objtype)) @
(opt_attr "thyname" thyname) @
(opt_attr "name" name),
(map idtable_to_xml idtables) @
--- a/src/Pure/ProofGeneral/pgml.ML Tue Oct 20 23:25:04 2009 +0200
+++ b/src/Pure/ProofGeneral/pgml.ML Wed Oct 21 00:36:12 2009 +0200
@@ -155,6 +155,6 @@
XML.Elem("pgml",
opt_attr "version" version @
opt_attr "systemid" systemid @
- Option.getOpt(Option.map PgipTypes.attrs_of_displayarea area,[]),
+ the_default [] (Option.map PgipTypes.attrs_of_displayarea area),
map pgmlterm_to_xml content)
end