src/HOL/Tools/res_hol_clause.ML
changeset 30153 051d3825a15d
parent 30151 629f3a92863e
child 30190 479806475f3c
     1.1 --- a/src/HOL/Tools/res_hol_clause.ML	Fri Feb 27 18:50:35 2009 +0100
     1.2 +++ b/src/HOL/Tools/res_hol_clause.ML	Fri Feb 27 19:19:39 2009 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4    val comb_C: thm
     1.5    val comb_S: thm
     1.6    datatype type_level = T_FULL | T_CONST
     1.7 -  val typ_level: type_level ref
     1.8 -  val minimize_applies: bool ref
     1.9 +  val typ_level: type_level
    1.10 +  val minimize_applies: bool
    1.11    type axiom_name = string
    1.12    type polarity = bool
    1.13    type clause_id = int
    1.14 @@ -53,17 +53,17 @@
    1.15  (*The different translations of types*)
    1.16  datatype type_level = T_FULL | T_CONST;
    1.17  
    1.18 -val typ_level = ref T_CONST;
    1.19 +val typ_level = T_CONST;
    1.20  
    1.21  (*If true, each function will be directly applied to as many arguments as possible, avoiding
    1.22    use of the "apply" operator. Use of hBOOL is also minimized.*)
    1.23 -val minimize_applies = ref true;
    1.24 +val minimize_applies = true;
    1.25  
    1.26  fun min_arity_of const_min_arity c = getOpt (Symtab.lookup const_min_arity c, 0);
    1.27  
    1.28  (*True if the constant ever appears outside of the top-level position in literals.
    1.29    If false, the constant always receives all of its arguments and is used as a predicate.*)
    1.30 -fun needs_hBOOL const_needs_hBOOL c = not (!minimize_applies) orelse
    1.31 +fun needs_hBOOL const_needs_hBOOL c = not minimize_applies orelse
    1.32                      getOpt (Symtab.lookup const_needs_hBOOL c, false);
    1.33  
    1.34  
    1.35 @@ -219,7 +219,7 @@
    1.36    | head_needs_hBOOL const_needs_hBOOL _ = true;
    1.37  
    1.38  fun wrap_type (s, tp) =
    1.39 -  if !typ_level=T_FULL then
    1.40 +  if typ_level=T_FULL then
    1.41        type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp]
    1.42    else s;
    1.43  
    1.44 @@ -240,7 +240,7 @@
    1.45                                           Int.toString nargs ^ " but is applied to " ^
    1.46                                           space_implode ", " args)
    1.47            val args2 = List.drop(args, nargs)
    1.48 -          val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars
    1.49 +          val targs = if typ_level = T_CONST then map RC.string_of_fol_type tvars
    1.50                        else []
    1.51        in
    1.52            string_apply (c ^ RC.paren_pack (args1@targs), args2)
    1.53 @@ -334,7 +334,7 @@
    1.54        if c = "equal" then (addtypes tvars funcs, preds)
    1.55        else
    1.56  	let val arity = min_arity_of cma c
    1.57 -	    val ntys = if !typ_level = T_CONST then length tvars else 0
    1.58 +	    val ntys = if typ_level = T_CONST then length tvars else 0
    1.59  	    val addit = Symtab.update(c, arity+ntys)
    1.60  	in
    1.61  	    if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
    1.62 @@ -449,7 +449,7 @@
    1.63                  (if needs_hBOOL const_needs_hBOOL c then " needs hBOOL" else ""));
    1.64  
    1.65  fun count_constants (conjectures, axclauses, helper_clauses) =
    1.66 -  if !minimize_applies then
    1.67 +  if minimize_applies then
    1.68       let val (const_min_arity, const_needs_hBOOL) =
    1.69            fold count_constants_clause conjectures (Symtab.empty, Symtab.empty)
    1.70         |> fold count_constants_clause axclauses