src/Tools/Code/code_thingol.ML
changeset 33029 2fefe039edf1
parent 32929 0e9e13ac06d7
child 33172 61ee96bc9895
     1.1 --- a/src/Tools/Code/code_thingol.ML	Tue Oct 20 20:03:23 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Tue Oct 20 20:54:31 2009 +0200
     1.3 @@ -420,7 +420,7 @@
     1.4  fun same_arity thy thms =
     1.5    let
     1.6      val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
     1.7 -    val k = fold (curry Int.max o num_args_of o Thm.prop_of) thms 0;
     1.8 +    val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
     1.9    in map (expand_eta thy k) thms end;
    1.10  
    1.11  fun mk_desymbolization pre post mk vs =