src/Pure/Proof/extraction.ML
changeset 14472 cba7c0a3ffb3
parent 13793 c02c81fd11b8
child 14854 61bdf2ae4dc5
--- a/src/Pure/Proof/extraction.ML	Wed Mar 17 14:00:45 2004 +0100
+++ b/src/Pure/Proof/extraction.ML	Fri Mar 19 10:42:38 2004 +0100
@@ -110,7 +110,7 @@
           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;