tuned;

--- a/src/Provers/Arith/fast_lin_arith.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -430,11 +430,10 @@
       fun addthms thm1 thm2 =
         case add2 thm1 thm2 of
           NONE => (case try_add ([thm1] RL inj_thms) thm2 of
-                     NONE => ( valOf(try_add ([thm2] RL inj_thms) thm1)
+                     NONE => (the (try_add ([thm2] RL inj_thms) thm1)
                                handle Option =>
                                (trace_thm "" thm1; trace_thm "" thm2;
-                                sys_error "Lin.arith. failed to add thms")
-                             )
+                                sys_error "Lin.arith. failed to add thms"))
                    | SOME thm => thm)
         | SOME thm => thm;
 

--- a/src/Provers/blast.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Provers/blast.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -650,7 +650,7 @@
           | 1 => immediate_output"\t1 variable UPDATED:"
           | n => immediate_output("\t" ^ Int.toString n ^ " variables UPDATED:");
        (*display the instantiations themselves, though no variable names*)
-       List.app (fn v => immediate_output("   " ^ string_of sign 4 (valOf (!v))))
+       List.app (fn v => immediate_output("   " ^ string_of sign 4 (the (!v))))
            (List.take(!trail, !ntrail-ntrl));
        writeln"")
     else ();

--- a/src/Pure/IsaPlanner/term_lib.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/IsaPlanner/term_lib.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -354,14 +354,9 @@
     if ty1 = ty2 then term_name_eq t1 t2 l
     else NONE
   | term_name_eq (ah $ at) (bh $ bt) l =
-    let
-      val lopt = (term_name_eq ah bh l)
-    in
-      if isSome lopt then
-	      term_name_eq at bt (valOf lopt)
-      else
-        NONE
-    end
+      (case term_name_eq ah bh l of
+        NONE => NONE
+      | SOME l' => term_name_eq at bt l')
   | term_name_eq (Const(a,T)) (Const(b,U)) l =
     if a=b andalso T=U then SOME l
     else NONE
@@ -380,12 +375,12 @@
  (* checks to see if the term in a name-equivalent member of the list of terms. *)
   fun get_name_eq_member a [] = NONE
     | get_name_eq_member a (h :: t) =
-        if isSome (term_name_eq a h []) then SOME h
+        if is_some (term_name_eq a h []) then SOME h
 				else get_name_eq_member a t;
 
   fun name_eq_member a [] = false
     | name_eq_member a (h :: t) =
-        if isSome (term_name_eq a h []) then true
+        if is_some (term_name_eq a h []) then true
 				else name_eq_member a t;
 
   (* true if term is a variable *)

--- a/src/Pure/Isar/find_theorems.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -204,7 +204,7 @@
   | filter_crit ctxt _ (Simp pat) = filter_simp ctxt pat
   | filter_crit ctxt _ (Pattern pat) = filter_pattern ctxt pat;
 
-fun opt_not x = if isSome x then NONE else SOME (0, 0);
+fun opt_not x = if is_some x then NONE else SOME (0, 0);
 
 fun opt_add (SOME (a, x)) (SOME (b, y)) = SOME (Int.max (a, b), x + y : int)
  |  opt_add _ _ = NONE;

--- a/src/Pure/Tools/compute.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/Tools/compute.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -177,7 +177,7 @@
 
                 fun make_pattern table invtable n vars (var as AbstractMachine.Var v) =
                     let
-                        val var' = valOf (AMTermTab.lookup invtable var)
+                        val var' = the (AMTermTab.lookup invtable var)
                         val table = Termtab.delete var' table
                         val invtable = AMTermTab.delete var invtable
                         val vars = Inttab.update_new (v, n) vars handle Inttab.DUP _ =>

--- a/src/Pure/codegen.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/codegen.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -1011,8 +1011,9 @@
     val (gi, frees) = Logic.goal_params
       (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
     val gi' = ObjectLogic.atomize_term thy (map_term_types
-      (map_type_tfree (fn p as (s, _) => getOpt (AList.lookup (op =) tvinsts s,
-        getOpt (default_type, TFree p)))) (subst_bounds (frees, strip gi)));
+      (map_type_tfree (fn p as (s, _) =>
+        the_default (the_default (TFree p) default_type)
+          (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
   in case test_term (Toplevel.theory_of st) size iterations gi' of
       NONE => writeln "No counterexamples found."
     | SOME cex => writeln ("Counterexample found:\n" ^
@@ -1189,8 +1190,7 @@
     (   parse_test_params >> (fn f => fn thy => apfst (f thy))
      || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
     (fn (ps, g) => Toplevel.keep (fn st =>
-      test_goal (app (getOpt (Option.map
-          (map (fn f => f (Toplevel.theory_of st))) ps, []))
+      test_goal (app (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
         (get_test_params (Toplevel.theory_of st), [])) g st)));
 
 val valueP =

--- a/src/Pure/consts.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/consts.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -236,7 +236,7 @@
     fun abbrev (xs, body) =
       let val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []
       in (Term.subst_bounds (rev vars, body), Term.list_comb (Const const, vars)) end;
-  in map abbrev (rev (strip_abss (Envir.beta_eta_contract rhs))) end;
+  in map abbrev (strip_abss (Envir.beta_eta_contract rhs)) end;
 
 in
 
@@ -254,8 +254,7 @@
         val decls' = decls
           |> extend_decls naming (c, (((T, Abbreviation rhs'), early), stamp ()));
         val rev_abbrevs' = rev_abbrevs
-          |> Symtab.default (mode, [])
-          |> Symtab.map_entry mode (append (rev_abbrev (NameSpace.full naming c, T) rhs));
+          |> fold (curry Symtab.update_list mode) (rev_abbrev (NameSpace.full naming c, T) rhs);
       in (decls', constraints, rev_abbrevs', expand_abbrevs) end)
   end;
 

--- a/src/Pure/meta_simplifier.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/meta_simplifier.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -552,7 +552,7 @@
       val (lhs, _) = Drule.dest_equals (Drule.strip_imp_concl (Thm.cprop_of thm))
         handle TERM _ => raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     (*val lhs = Envir.eta_contract lhs;*)
-      val a = valOf (cong_name (head_of (term_of lhs))) handle Option =>
+      val a = the (cong_name (head_of (term_of lhs))) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant or free variable", thm);
       val (alist, weak) = congs;
       val alist2 = overwrite_warn (alist, (a, {lhs = lhs, thm = thm}))
@@ -566,7 +566,7 @@
       val (lhs, _) = Logic.dest_equals (Thm.concl_of thm) handle TERM _ =>
         raise SIMPLIFIER ("Congruence not a meta-equality", thm);
     (*val lhs = Envir.eta_contract lhs;*)
-      val a = valOf (cong_name (head_of lhs)) handle Option =>
+      val a = the (cong_name (head_of lhs)) handle Option =>
         raise SIMPLIFIER ("Congruence must start with a constant", thm);
       val (alist, _) = congs;
       val alist2 = List.filter (fn (x, _) => x <> a) alist;
@@ -1010,7 +1010,7 @@
     may be a redex. Example: map (%x. x) = (%xs. xs) wrt map_cong*)
                           (let
                              val thm = congc (prover ss) ss maxidx cong t0;
-                             val t = getOpt (Option.map rhs_of thm, t0);
+                             val t = the_default t0 (Option.map rhs_of thm);
                              val (cl, cr) = Thm.dest_comb t
                              val dVar = Var(("", 0), dummyT)
                              val skel =
@@ -1062,12 +1062,12 @@
           let
             val ss' = add_rrules (rev rrss, rev asms) ss;
             val concl' =
-              Drule.mk_implies (prem, getOpt (Option.map rhs_of eq, concl));
+              Drule.mk_implies (prem, the_default concl (Option.map rhs_of eq));
             val dprem = Option.map (curry (disch false) prem)
           in case rewritec (prover, thy, maxidx) ss' concl' of
               NONE => rebuild prems concl' rrss asms ss (dprem eq)
             | SOME (eq', _) => transitive2 (Library.foldl (disch false o swap)
-                  (valOf (transitive3 (dprem eq) eq'), prems))
+                  (the (transitive3 (dprem eq) eq'), prems))
                 (mut_impc0 (rev prems) (rhs_of eq') (rev rrss) (rev asms) ss)
           end
 
@@ -1112,7 +1112,7 @@
      and nonmut_impc ct ss =
        let val (prem, conc) = dest_implies ct;
            val thm1 = if simprem then botc skel0 ss prem else NONE;
-           val prem1 = getOpt (Option.map rhs_of thm1, prem);
+           val prem1 = the_default prem (Option.map rhs_of thm1);
            val ss1 = if not useprem then ss else add_rrules
              (apsnd single (apfst single (rules_of_prem ss prem1))) ss
        in (case botc skel0 ss1 conc of

--- a/src/Pure/pattern.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/pattern.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -153,7 +153,7 @@
 
 (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
 fun mk_proj_list is =
-    let fun mk(i::is,j) = if isSome i then j :: mk(is,j-1) else mk(is,j-1)
+    let fun mk(i::is,j) = if is_some i then j :: mk(is,j-1) else mk(is,j-1)
           | mk([],_)    = []
     in mk(is,length is - 1) end;
 

--- a/src/Pure/proofterm.ML	Fri Apr 28 17:59:06 2006 +0200
+++ b/src/Pure/proofterm.ML	Sat Apr 29 23:16:43 2006 +0200
@@ -784,7 +784,7 @@
   abstract_rule_axm % NONE % NONE %% forall_intr_proof x a prf;
 
 fun check_comb (PAxm ("ProtoPure.combination", _, _) % f % g % _ % _ %% prf %% _) =
-      isSome f orelse check_comb prf
+      is_some f orelse check_comb prf
   | check_comb (PAxm ("ProtoPure.transitive", _, _) % _ % _ % _ %% prf1 %% prf2) =
       check_comb prf1 andalso check_comb prf2
   | check_comb (PAxm ("ProtoPure.symmetric", _, _) % _ % _ %% prf) = check_comb prf
@@ -1099,27 +1099,27 @@
           if prf_loose_Pbvar1 prf' 0 then rew Ts prf
           else
             let val prf'' = incr_pboundvars (~1) 0 prf'
-            in SOME (getOpt (rew Ts prf'', (prf'', skel0))) end
+            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
       | rew0 Ts (prf as Abst (_, _, prf' % SOME (Bound 0))) =
           if prf_loose_bvar1 prf' 0 then rew Ts prf
           else
             let val prf'' = incr_pboundvars 0 (~1) prf'
-            in SOME (getOpt (rew Ts prf'', (prf'', skel0))) end
+            in SOME (the_default (prf'', skel0) (rew Ts prf'')) end
       | rew0 Ts prf = rew Ts prf;
 
     fun rew1 _ (Hyp (Var _)) _ = NONE
       | rew1 Ts skel prf = (case rew2 Ts skel prf of
           SOME prf1 => (case rew0 Ts prf1 of
-              SOME (prf2, skel') => SOME (getOpt (rew1 Ts skel' prf2, prf2))
+              SOME (prf2, skel') => SOME (the_default prf2 (rew1 Ts skel' prf2))
             | NONE => SOME prf1)
         | NONE => (case rew0 Ts prf of
-              SOME (prf1, skel') => SOME (getOpt (rew1 Ts skel' prf1, prf1))
+              SOME (prf1, skel') => SOME (the_default prf1 (rew1 Ts skel' prf1))
             | NONE => NONE))
 
     and rew2 Ts skel (prf % SOME t) = (case prf of
             Abst (_, _, body) =>
               let val prf' = prf_subst_bounds [t] body
-              in SOME (getOpt (rew2 Ts skel0 prf', prf')) end
+              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
           | _ => (case rew1 Ts (case skel of skel' % _ => skel' | _ => skel0) prf of
               SOME prf' => SOME (prf' % SOME t)
             | NONE => NONE))
@@ -1128,7 +1128,7 @@
       | rew2 Ts skel (prf1 %% prf2) = (case prf1 of
             AbsP (_, _, body) =>
               let val prf' = prf_subst_pbounds [prf2] body
-              in SOME (getOpt (rew2 Ts skel0 prf', prf')) end
+              in SOME (the_default prf' (rew2 Ts skel0 prf')) end
           | _ =>
             let val (skel1, skel2) = (case skel of
                 skel1 %% skel2 => (skel1, skel2)
@@ -1141,7 +1141,7 @@
                     SOME prf2' => SOME (prf1 %% prf2')
                   | NONE => NONE)
             end)
-      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (getOpt (T,dummyT) :: Ts)
+      | rew2 Ts skel (Abst (s, T, prf)) = (case rew1 (the_default dummyT T :: Ts)
               (case skel of Abst (_, _, skel') => skel' | _ => skel0) prf of
             SOME prf' => SOME (Abst (s, T, prf'))
           | NONE => NONE)
@@ -1151,7 +1151,7 @@
           | NONE => NONE)
       | rew2 _ _ _ = NONE
 
-  in getOpt (rew1 [] skel0 prf, prf) end;
+  in the_default prf (rew1 [] skel0 prf) end;
 
 fun rewrite_proof thy = rewrite_prf (fn (tyenv, f) =>
   Sign.typ_match thy (f ()) tyenv handle Type.TYPE_MATCH => raise PMatch);