merged

--- a/src/Pure/General/integer.ML	Wed Nov 08 15:31:14 2017 +0100
+++ b/src/Pure/General/integer.ML	Wed Nov 08 17:36:21 2017 +0100
@@ -40,20 +40,7 @@
 
 fun square x = x * x;
 
-fun pow k l =
-  let
-    fun pw 0 _ = 1
-      | pw 1 l = l
-      | pw k l =
-          let
-            val (k', r) = div_mod k 2;
-            val l' = pw k' (l * l);
-          in if r = 0 then l' else l' * l end;
-  in
-    if k < 0
-    then IntInf.pow (l, k)
-    else pw k l
-  end;
+fun pow k l = IntInf.pow (l, k);
 
 fun gcd x y = PolyML.IntInf.gcd (x, y);
 fun lcm x y = abs (PolyML.IntInf.lcm (x, y));
@@ -65,10 +52,3 @@
   | lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
 
 end;
-
-(* FIXME workaround for Poly/ML 5.7.1 testing *)
-structure IntInf =
-struct
-  open IntInf;
-  fun pow (i, n) = Integer.pow n i;
-end

--- a/src/Pure/Pure.thy	Wed Nov 08 15:31:14 2017 +0100
+++ b/src/Pure/Pure.thy	Wed Nov 08 17:36:21 2017 +0100
@@ -120,6 +120,8 @@
       in () end)));
 \<close>
 
+external_file "$POLYML_EXE"
+
 
 subsection \<open>Embedded ML text\<close>