src/Pure/tactic.ML
changeset 18977 f24c416a4814
parent 18500 8b1a4e8ed199
child 19056 6ac9dfe98e54
     1.1 --- a/src/Pure/tactic.ML	Wed Feb 08 09:27:20 2006 +0100
     1.2 +++ b/src/Pure/tactic.ML	Wed Feb 08 14:39:00 2006 +0100
     1.3 @@ -567,7 +567,7 @@
     1.4    Returns longest lhs first to avoid folding its subexpressions.*)
     1.5  fun sort_lhs_depths defs =
     1.6    let val keylist = AList.make (term_depth o lhs_of_thm) defs
     1.7 -      val keys = distinct (sort (rev_order o int_ord) (map #2 keylist))
     1.8 +      val keys = gen_distinct (op =) (sort (rev_order o int_ord) (map #2 keylist))
     1.9    in map (AList.find (op =) keylist) keys end;
    1.10  
    1.11  val rev_defs = sort_lhs_depths o map symmetric;