src/Pure/Proof/extraction.ML

            iTs = Vartab.make Tenv, asol = Vartab.make tenv};
         val env'' = foldl (fn (env, p) =>
           Pattern.unify (sign, env, [pairself rew p])) (env', prems')
       in Some (Envir.norm_term env'' (inc (ren tm2)))
       end handle Pattern.MATCH => None | Pattern.Unif => None)
-        (sort (int_ord o pairself fst)
+        (sort (Int.compare o pairself fst)
           (Net.match_term rules (Pattern.eta_contract tm)));
 
   in rew end;
 
 val chtype = change_type o Some;