# HG changeset patch
# User wenzelm
# Date 1303221485 -7200
# Node ID 38b29c9fc742c48953ac8f9353779292bc8f9b7c
# Parent  c7139609b67db6936f684ada2add0886e52dc88c
slightly more special eq_list/eq_set, with shortcut involving pointer_eq;

diff -r c7139609b67d -r 38b29c9fc742 NEWS
--- a/NEWS	Tue Apr 19 14:57:09 2011 +0200
+++ b/NEWS	Tue Apr 19 15:58:05 2011 +0200
@@ -115,6 +115,9 @@
 * Refined PARALLEL_GOALS tactical: degrades gracefully for schematic
 goal states; body tactic needs to address all subgoals uniformly.
 
+* Slightly more special eq_list/eq_set, with shortcut involving
+pointer equality (assumes that eq relation is reflexive).
+
 
 
 New in Isabelle2011 (January 2011)
diff -r c7139609b67d -r 38b29c9fc742 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Tue Apr 19 14:57:09 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Apr 19 15:58:05 2011 +0200
@@ -275,10 +275,8 @@
   Checks.map (which (AList.map_default op = (key, []) (cons ((name, f), stamp ()))));
 
 fun simple_check eq f xs ctxt =
-  let val xs' = f ctxt xs in
-    if pointer_eq (xs, xs') orelse eq_list eq (xs, xs') then NONE
-    else SOME (xs', ctxt)
-  end;
+  let val xs' = f ctxt xs
+  in if eq_list eq (xs, xs') then NONE else SOME (xs', ctxt) end;
 
 in
 
diff -r c7139609b67d -r 38b29c9fc742 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Apr 19 14:57:09 2011 +0200
+++ b/src/Pure/library.ML	Tue Apr 19 15:58:05 2011 +0200
@@ -93,7 +93,7 @@
   val find_first: ('a -> bool) -> 'a list -> 'a option
   val get_index: ('a -> 'b option) -> 'a list -> (int * 'b) option
   val get_first: ('a -> 'b option) -> 'a list -> 'b option
-  val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val eq_list: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
@@ -168,7 +168,7 @@
   val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
-  val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val eq_set: ('a * 'a -> bool) -> 'a list * 'a list -> bool
   val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
@@ -396,10 +396,11 @@
 (* basic list functions *)
 
 fun eq_list eq (list1, list2) =
-  let
-    fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
-      | eq_lst _ = true;
-  in length list1 = length list2 andalso eq_lst (list1, list2) end;
+  pointer_eq (list1, list2) orelse
+    let
+      fun eq_lst (x :: xs, y :: ys) = eq (x, y) andalso eq_lst (xs, ys)
+        | eq_lst _ = true;
+    in length list1 = length list2 andalso eq_lst (list1, list2) end;
 
 fun maps f [] = []
   | maps f (x :: xs) = f x @ maps f xs;