src/Pure/tactic.ML
changeset 17496 26535df536ae
parent 17271 2756a73f63a5
child 17851 2fa4f9b54761
     1.1 --- a/src/Pure/tactic.ML	Tue Sep 20 08:20:22 2005 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Sep 20 08:21:49 2005 +0200
     1.3 @@ -573,9 +573,9 @@
     1.4  (*folding should handle critical pairs!  E.g. K == Inl(0),  S == Inr(Inl(0))
     1.5    Returns longest lhs first to avoid folding its subexpressions.*)
     1.6  fun sort_lhs_depths defs =
     1.7 -  let val keylist = make_keylist (term_depth o lhs_of_thm) defs
     1.8 +  let val keylist = AList.make (term_depth o lhs_of_thm) defs
     1.9        val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
    1.10 -  in  map (keyfilter keylist) keys  end;
    1.11 +  in map (AList.find (op =) keylist) keys end;
    1.12  
    1.13  val rev_defs = sort_lhs_depths o map symmetric;
    1.14