tuned;
authorwenzelm
Mon Feb 06 20:59:06 2006 +0100 (2006-02-06)
changeset 1893918e2a2676d80
parent 18938 b401ee1cda14
child 18940 d8e12bf337a3
tuned;
src/Pure/General/name_space.ML
src/Pure/General/symbol.ML
src/Pure/Isar/find_theorems.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/net.ML
src/Pure/type_infer.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Feb 06 20:59:05 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Feb 06 20:59:06 2006 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  (* basic operations *)
     1.5  
     1.6  fun map_space f xname (NameSpace tab) =
     1.7 -  NameSpace (Symtab.update (xname, f (if_none (Symtab.lookup tab xname) ([], []))) tab);
     1.8 +  NameSpace (Symtab.update (xname, f (the_default ([], []) (Symtab.lookup tab xname))) tab);
     1.9  
    1.10  fun del (name: string) = remove (op =) name;
    1.11  fun add name names = name :: del name names;
    1.12 @@ -179,7 +179,7 @@
    1.13  
    1.14  fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
    1.15    xname |> map_space (fn (names2, names2') =>
    1.16 -    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
    1.17 +    (Library.merge (op =) (names2, names1), Library.merge (op =) (names2', names1')))) tab1 space2;
    1.18  
    1.19  
    1.20  
     2.1 --- a/src/Pure/General/symbol.ML	Mon Feb 06 20:59:05 2006 +0100
     2.2 +++ b/src/Pure/General/symbol.ML	Mon Feb 06 20:59:06 2006 +0100
     2.3 @@ -351,7 +351,7 @@
     2.4      else if is_ascii_quasi s then Quasi
     2.5      else if is_ascii_blank s then Blank
     2.6      else if is_char s then Other
     2.7 -    else if_none (Symtab.lookup symbol_kinds s) Other;
     2.8 +    else the_default Other (Symtab.lookup symbol_kinds s);
     2.9  end;
    2.10  
    2.11  fun is_letter s = kind s = Letter;
     3.1 --- a/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:05 2006 +0100
     3.2 +++ b/src/Pure/Isar/find_theorems.ML	Mon Feb 06 20:59:06 2006 +0100
     3.3 @@ -139,7 +139,7 @@
     3.4      val concl = Logic.concl_of_goal goal 1;
     3.5      val ss = is_matching_thm extract_intro ctxt true concl thm;
     3.6    in
     3.7 -    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
     3.8 +    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
     3.9    end;
    3.10  
    3.11  fun filter_elim ctxt goal (_, thm) =
    3.12 @@ -176,7 +176,7 @@
    3.13        (map Thm.full_prop_of o mk, #1 o Logic.dest_equals o Logic.strip_imp_concl);
    3.14      val ss = is_matching_thm extract_simp ctxt false t thm
    3.15    in
    3.16 -    if is_some ss then SOME (Thm.nprems_of thm, valOf ss) else NONE
    3.17 +    if is_some ss then SOME (Thm.nprems_of thm, the ss) else NONE
    3.18    end;
    3.19  
    3.20  
     4.1 --- a/src/Pure/Isar/method.ML	Mon Feb 06 20:59:05 2006 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Mon Feb 06 20:59:06 2006 +0100
     4.3 @@ -176,7 +176,7 @@
     4.4  (* shuffle subgoals *)
     4.5  
     4.6  fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
     4.7 -fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
     4.8 +fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
     4.9  
    4.10  
    4.11  (* cheating *)
    4.12 @@ -333,7 +333,7 @@
    4.13  in
    4.14  
    4.15  fun iprover_tac ctxt opt_lim =
    4.16 -  SELECT_GOAL (DEEPEN (2, if_none opt_lim 20) (intprover_tac ctxt [] 0) 4 1);
    4.17 +  SELECT_GOAL (DEEPEN (2, the_default 20 opt_lim) (intprover_tac ctxt [] 0) 4 1);
    4.18  
    4.19  end;
    4.20  
     5.1 --- a/src/Pure/Isar/object_logic.ML	Mon Feb 06 20:59:05 2006 +0100
     5.2 +++ b/src/Pure/Isar/object_logic.ML	Mon Feb 06 20:59:06 2006 +0100
     5.3 @@ -105,7 +105,7 @@
     5.4      val c = judgment_name thy;
     5.5      val aT = TFree ("'a", []);
     5.6      val T =
     5.7 -      if_none (Sign.const_type thy c) (aT --> propT)
     5.8 +      the_default (aT --> propT) (Sign.const_type thy c)
     5.9        |> Term.map_type_tvar (fn ((x, _), S) => TFree (x, S));
    5.10      val U = Term.domain_type T handle Match => aT;
    5.11    in Const (c, T) $ Free (x, U) end;
     6.1 --- a/src/Pure/Proof/proof_syntax.ML	Mon Feb 06 20:59:05 2006 +0100
     6.2 +++ b/src/Pure/Proof/proof_syntax.ML	Mon Feb 06 20:59:06 2006 +0100
     6.3 @@ -192,17 +192,17 @@
     6.4        mk_tyapp (Const (NameSpace.append "axm" name, proofT), Ts)
     6.5    | term_of _ (PBound i) = Bound i
     6.6    | term_of Ts (Abst (s, opT, prf)) = 
     6.7 -      let val T = getOpt (opT,dummyT)
     6.8 +      let val T = the_default dummyT opT
     6.9        in Const ("Abst", (T --> proofT) --> proofT) $
    6.10          Abs (s, T, term_of (T::Ts) (incr_pboundvars 1 0 prf))
    6.11        end
    6.12    | term_of Ts (AbsP (s, t, prf)) =
    6.13 -      AbsPt $ getOpt (t, Const ("dummy_pattern", propT)) $
    6.14 +      AbsPt $ the_default (Term.dummy_pattern propT) t $
    6.15          Abs (s, proofT, term_of (proofT::Ts) (incr_pboundvars 0 1 prf))
    6.16    | term_of Ts (prf1 %% prf2) =
    6.17        AppPt $ term_of Ts prf1 $ term_of Ts prf2
    6.18    | term_of Ts (prf % opt) = 
    6.19 -      let val t = getOpt (opt, Const ("dummy_pattern", dummyT))
    6.20 +      let val t = the_default (Term.dummy_pattern dummyT) opt
    6.21        in Const ("Appt",
    6.22          [proofT, fastype_of1 (Ts, t) handle TERM _ => dummyT] ---> proofT) $
    6.23            term_of Ts prf $ t
     7.1 --- a/src/Pure/net.ML	Mon Feb 06 20:59:05 2006 +0100
     7.2 +++ b/src/Pure/net.ML	Mon Feb 06 20:59:06 2006 +0100
     7.3 @@ -94,7 +94,7 @@
     7.4              Net{comb=comb, var=ins1(keys,var), atoms=atoms}
     7.5          | ins1 (AtomK a :: keys, Net{comb,var,atoms}) =
     7.6              let
     7.7 -              val net' = if_none (Symtab.lookup atoms a) empty;
     7.8 +              val net' = the_default empty (Symtab.lookup atoms a);
     7.9                val atoms' = Symtab.update (a, ins1 (keys, net')) atoms;
    7.10              in  Net{comb=comb, var=var, atoms=atoms'}  end
    7.11    in  ins1 (keys,net)  end;
    7.12 @@ -222,7 +222,7 @@
    7.13            subtr comb1 comb2
    7.14            #> subtr var1 var2
    7.15            #> Symtab.fold (fn (a, net) =>
    7.16 -            subtr (if_none (Symtab.lookup atoms1 a) emptynet) net) atoms2
    7.17 +            subtr (the_default emptynet (Symtab.lookup atoms1 a)) net) atoms2
    7.18    in subtr net1 net2 [] end;
    7.19  
    7.20  fun entries net = subtract (K false) empty net;
     8.1 --- a/src/Pure/type_infer.ML	Mon Feb 06 20:59:05 2006 +0100
     8.2 +++ b/src/Pure/type_infer.ML	Mon Feb 06 20:59:06 2006 +0100
     8.3 @@ -482,7 +482,7 @@
     8.4  
     8.5  fun decode_types tsig is_const def_type def_sort map_const map_type map_sort tm =
     8.6    let
     8.7 -    fun get_type xi = if_none (def_type xi) dummyT;
     8.8 +    fun get_type xi = the_default dummyT (def_type xi);
     8.9      fun is_free x = is_some (def_type (x, ~1));
    8.10      val raw_env = Syntax.raw_term_sorts tm;
    8.11      val sort_of = get_sort tsig def_sort map_sort raw_env;