merged
authorwenzelm
Wed Nov 08 17:36:21 2017 +0100 (19 months ago)
changeset 670358b7233175199
parent 67032 ed499d1252fc
parent 67034 09fb749d1a1e
child 67037 a76fb0f4b9ca
merged
     1.1 --- a/src/Pure/General/integer.ML	Wed Nov 08 15:31:14 2017 +0100
     1.2 +++ b/src/Pure/General/integer.ML	Wed Nov 08 17:36:21 2017 +0100
     1.3 @@ -40,20 +40,7 @@
     1.4  
     1.5  fun square x = x * x;
     1.6  
     1.7 -fun pow k l =
     1.8 -  let
     1.9 -    fun pw 0 _ = 1
    1.10 -      | pw 1 l = l
    1.11 -      | pw k l =
    1.12 -          let
    1.13 -            val (k', r) = div_mod k 2;
    1.14 -            val l' = pw k' (l * l);
    1.15 -          in if r = 0 then l' else l' * l end;
    1.16 -  in
    1.17 -    if k < 0
    1.18 -    then IntInf.pow (l, k)
    1.19 -    else pw k l
    1.20 -  end;
    1.21 +fun pow k l = IntInf.pow (l, k);
    1.22  
    1.23  fun gcd x y = PolyML.IntInf.gcd (x, y);
    1.24  fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
    1.25 @@ -65,10 +52,3 @@
    1.26    | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
    1.27  
    1.28  end;
    1.29 -
    1.30 -(* FIXME workaround for Poly/ML 5.7.1 testing *)
    1.31 -structure IntInf =
    1.32 -struct
    1.33 -  open IntInf;
    1.34 -  fun pow (i, n) = Integer.pow n i;
    1.35 -end
     2.1 --- a/src/Pure/Pure.thy	Wed Nov 08 15:31:14 2017 +0100
     2.2 +++ b/src/Pure/Pure.thy	Wed Nov 08 17:36:21 2017 +0100
     2.3 @@ -120,6 +120,8 @@
     2.4        in () end)));
     2.5  \<close>
     2.6  
     2.7 +external_file "$POLYML_EXE"
     2.8 +
     2.9  
    2.10  subsection \<open>Embedded ML text\<close>
    2.11