src/HOL/Tools/res_hol_clause.ML
changeset 33035 15eab423e573
parent 33029 2fefe039edf1
child 33039 5018f6a76b3f
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Tue Oct 20 23:25:04 2009 +0200
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Wed Oct 21 00:36:12 2009 +0200
     1.3 @@ -69,12 +69,13 @@
     1.4    use of the "apply" operator. Use of hBOOL is also minimized.*)
     1.5  val minimize_applies = true;
     1.6  
     1.7 -fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
     1.8 +fun min_arity_of const_min_arity c = the_default 0 (Symtab.lookup const_min_arity c);
     1.9  
    1.10  (*True if the constant ever appears outside of the top-level position in literals.
    1.11    If false, the constant always receives all of its arguments and is used as a predicate.*)
    1.12 -fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
    1.13 -                    getOpt (Symtab.lookup const_needs_hBOOL c, false);
    1.14 +fun needs_hBOOL const_needs_hBOOL c =
    1.15 +  not minimize_applies orelse
    1.16 +    the_default false (Symtab.lookup const_needs_hBOOL c);
    1.17  
    1.18  
    1.19  (******************************************************)
    1.20 @@ -412,7 +413,7 @@
    1.21          val axclauses = map #2 (make_axiom_clauses dfg thy axcls)
    1.22          val ct0 = List.foldl count_clause init_counters conjectures
    1.23          val ct = List.foldl (count_user_clause user_lemmas) ct0 axclauses
    1.24 -        fun needed c = valOf (Symtab.lookup ct c) > 0
    1.25 +        fun needed c = the (Symtab.lookup ct c) > 0
    1.26          val IK = if needed "c_COMBI" orelse needed "c_COMBK"
    1.27                   then cnf_helper_thms thy [comb_I,comb_K]
    1.28                   else []