src/HOL/Tools/lin_arith.ML
changeset 36001 992839c4be90
parent 35872 9b579860d59b
child 36692 54b64d4ad524
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Mar 28 16:13:29 2010 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 28 16:59:06 2010 +0200
     1.3 @@ -100,8 +100,8 @@
     1.4    {splits = splits, inj_consts = update (op =) c inj_consts,
     1.5     discrete = discrete});
     1.6  
     1.7 -val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" 9;
     1.8 -val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" 9;
     1.9 +val (split_limit, setup_split_limit) = Attrib.config_int "linarith_split_limit" (K 9);
    1.10 +val (neq_limit, setup_neq_limit) = Attrib.config_int "linarith_neq_limit" (K 9);
    1.11  
    1.12  
    1.13  structure LA_Data =