src/Pure/Proof/extraction.ML
changeset 14472 cba7c0a3ffb3
parent 13793 c02c81fd11b8
child 14854 61bdf2ae4dc5
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Mar 17 14:00:45 2004 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Fri Mar 19 10:42:38 2004 +0100
     1.3 @@ -110,7 +110,7 @@
     1.4            Pattern.unify (sign, env, [pairself rew p])) (env', prems')
     1.5        in Some (Envir.norm_term env'' (inc (ren tm2)))
     1.6        end handle Pattern.MATCH => None | Pattern.Unif => None)
     1.7 -        (sort (int_ord o pairself fst)
     1.8 +        (sort (Int.compare o pairself fst)
     1.9            (Net.match_term rules (Pattern.eta_contract tm)));
    1.10  
    1.11    in rew end;