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;