1.1 --- a/NEWS	Tue Apr 19 14:57:09 2011 +0200
     1.2 +++ b/NEWS	Tue Apr 19 15:58:05 2011 +0200
     1.3 @@ -115,6 +115,9 @@
     1.4  * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
     1.5  goal states; body tactic needs to address all subgoals uniformly.
     1.6  
     1.7 +* Slightly more special eq_list/eq_set, with shortcut involving
     1.8 +pointer equality (assumes that eq relation is reflexive).
     1.9 +
    1.10  
    1.11  
    1.12  New in Isabelle2011 (January 2011)

     2.1 --- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 15:58:05 2011 +0200
     2.3 @@ -275,10 +275,8 @@
     2.4    Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
     2.5  
     2.6  fun simple_check eq f xs ctxt =
     2.7 -  let val xs' = f ctxt xs in
     2.8 -    if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
     2.9 -    else SOME (xs', ctxt)
    2.10 -  end;
    2.11 +  let val xs' = f ctxt xs
    2.12 +  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
    2.13  
    2.14  in
    2.15  

     3.1 --- a/src/Pure/library.ML	Tue Apr 19 14:57:09 2011 +0200
     3.2 +++ b/src/Pure/library.ML	Tue Apr 19 15:58:05 2011 +0200
     3.3 @@ -93,7 +93,7 @@
     3.4    val find_first: ('a -> bool) -> 'a list -> 'a option
     3.5    val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
     3.6    val get_first: ('a -> 'b option) -> 'a list -> 'b option
     3.7 -  val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
     3.8 +  val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
     3.9    val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
    3.10    val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    3.11    val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
    3.12 @@ -168,7 +168,7 @@
    3.13    val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
    3.14    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    3.15    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    3.16 -  val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    3.17 +  val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
    3.18    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    3.19    val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
    3.20    val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
    3.21 @@ -396,10 +396,11 @@
    3.22  (* basic list functions *)
    3.23  
    3.24  fun eq_list eq (list1, list2) =
    3.25 -  let
    3.26 -    fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
    3.27 -      | eq_lst _ = true;
    3.28 -  in length list1 = length list2 andalso eq_lst (list1, list2) end;
    3.29 +  pointer_eq (list1, list2) orelse
    3.30 +    let
    3.31 +      fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
    3.32 +        | eq_lst _ = true;
    3.33 +    in length list1 = length list2 andalso eq_lst (list1, list2) end;
    3.34  
    3.35  fun maps f [] = []
    3.36    | maps f (x :: xs) = f x @ maps f xs;