changeset 41490 | 0f1e411a1448 |
parent 39557 | fe5722fce758 |
child 41491 | a2ad5b824051 |
--- a/src/HOL/Import/shuffler.ML Mon Jan 10 15:19:48 2011 +0100 +++ b/src/HOL/Import/shuffler.ML Mon Jan 10 15:30:17 2011 +0100 @@ -465,7 +465,7 @@ end | F (Abs(x,xT,t),idx) = let - val x' = "x" ^ (LargeInt.toString idx) (* amazing *) + val x' = "x" ^ Int.toString idx val (t',idx') = F (t,idx+1) in (Abs(x',xT,t'),idx')