tuned;

--- a/src/Pure/General/name_space.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/General/name_space.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -150,7 +150,7 @@
 (* basic operations *)
 
 fun map_space f xname (NameSpace tab) =
-  NameSpace (Symtab.update (xname, f (if_none (Symtab.lookup tab xname) ([], []))) tab);
+  NameSpace (Symtab.update (xname, f (the_default ([], []) (Symtab.lookup tab xname))) tab);
 
 fun del (name: string) = remove (op =) name;
 fun add name names = name :: del name names;
@@ -179,7 +179,7 @@
 
 fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
   xname |> map_space (fn (names2, names2') =>
-    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
+    (Library.merge (op =) (names2, names1), Library.merge (op =) (names2', names1')))) tab1 space2;
 
 
 

--- a/src/Pure/General/symbol.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/General/symbol.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -351,7 +351,7 @@
     else if is_ascii_quasi s then Quasi
     else if is_ascii_blank s then Blank
     else if is_char s then Other
-    else if_none (Symtab.lookup symbol_kinds s) Other;
+    else the_default Other (Symtab.lookup symbol_kinds s);
 end;
 
 fun is_letter s = kind s = Letter;

--- a/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -139,7 +139,7 @@
     val concl = Logic.concl_of_goal goal 1;
     val ss = is_matching_thm extract_intro ctxt true concl thm;
   in
-    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
+    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   end;
 
 fun filter_elim ctxt goal (_, thm) =
@@ -176,7 +176,7 @@
       (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
     val ss = is_matching_thm extract_simp ctxt false t thm
   in
-    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
+    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
   end;
 
 

--- a/src/Pure/Isar/method.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/Isar/method.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -176,7 +176,7 @@
 (* shuffle subgoals *)
 
 fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
+fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
 
 
 (* cheating *)
@@ -333,7 +333,7 @@
 in
 
 fun iprover_tac ctxt opt_lim =
-  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1);
+  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
 
 end;
 

--- a/src/Pure/Isar/object_logic.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -105,7 +105,7 @@
     val c = judgment_name thy;
     val aT = TFree ("'a", []);
     val T =
-      if_none (Sign.const_type thy c) (aT --> propT)
+      the_default (aT --> propT) (Sign.const_type thy c)
       |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
     val U = Term.domain_type T handle Match => aT;
   in Const (c, T) $ Free (x, U) end;

--- a/src/Pure/Proof/proof_syntax.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -192,17 +192,17 @@
       mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
   | term_of _ (PBound i) = Bound i
   | term_of Ts (Abst (s, opT, prf)) = 
-      let val T = getOpt (opT,dummyT)
+      let val T = the_default dummyT opT
       in Const ("Abst", (T --> proofT) --> proofT) $
         Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
       end
   | term_of Ts (AbsP (s, t, prf)) =
-      AbsPt $ getOpt (t, Const ("dummy_pattern", propT)) $
+      AbsPt $ the_default (Term.dummy_pattern propT) t $
         Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
   | term_of Ts (prf1 %% prf2) =
       AppPt $ term_of Ts prf1 $ term_of Ts prf2
   | term_of Ts (prf % opt) = 
-      let val t = getOpt (opt, Const ("dummy_pattern", dummyT))
+      let val t = the_default (Term.dummy_pattern dummyT) opt
       in Const ("Appt",
         [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
           term_of Ts prf $ t

--- a/src/Pure/net.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/net.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -94,7 +94,7 @@
             Net{comb=comb, var=ins1(keys,var), atoms=atoms}
         | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
             let
-              val net' = if_none (Symtab.lookup atoms a) empty;
+              val net' = the_default empty (Symtab.lookup atoms a);
               val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
             in  Net{comb=comb, var=var, atoms=atoms'}  end
   in  ins1 (keys,net)  end;
@@ -222,7 +222,7 @@
           subtr comb1 comb2
           #> subtr var1 var2
           #> Symtab.fold (fn (a, net) =>
-            subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2
+            subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
   in subtr net1 net2 [] end;
 
 fun entries net = subtract (K false) empty net;

--- a/src/Pure/type_infer.ML	Mon Feb 06 20:59:05 2006 +0100
+++ b/src/Pure/type_infer.ML	Mon Feb 06 20:59:06 2006 +0100
@@ -482,7 +482,7 @@
 
 fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
   let
-    fun get_type xi = if_none (def_type xi) dummyT;
+    fun get_type xi = the_default dummyT (def_type xi);
     fun is_free x = is_some (def_type (x, ~1));
     val raw_env = Syntax.raw_term_sorts tm;
     val sort_of = get_sort tsig def_sort map_sort raw_env;