# HG changeset patch
# User krauss
# Date 1163426519 -3600
# Node ID 9022a90f6fdd02a11b5510269b2a5f0031c66447
# Parent  d240748a2cf5488bd3bf233918b2068cee93c8f1
auto_term => lexicographic_order

diff -r d240748a2cf5 -r 9022a90f6fdd src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Nov 13 13:53:48 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Nov 13 15:01:59 2006 +0100
@@ -96,7 +96,8 @@
   "unionl [] ys = ys"
 | "unionl xs ys = foldr insertl xs ys"
 by pat_completeness auto
-termination unionl by (auto_term "{}")
+termination by lexicographic_order
+
 lemmas unionl_def = unionl.simps(2)
 declare unionl.simps[code]
 
@@ -105,8 +106,9 @@
   "intersect [] ys = []"
 | "intersect xs [] = []"
 | "intersect xs ys = filter (member xs) ys"
-  by pat_completeness auto
-termination intersect by (auto_term "{}")
+by pat_completeness auto
+termination by lexicographic_order
+
 lemmas intersect_def = intersect.simps(3)
 declare intersect.simps[code]
 
@@ -115,8 +117,9 @@
   "subtract [] ys = ys"
 | "subtract xs [] = []"
 | "subtract xs ys = foldr remove1 xs ys"
-  by pat_completeness auto
-termination subtract by (auto_term "{}")
+by pat_completeness auto
+termination by lexicographic_order
+
 lemmas subtract_def = subtract.simps(3)
 declare subtract.simps[code]
 
@@ -124,8 +127,9 @@
 where
   "map_distinct f [] = []"
 | "map_distinct f xs = foldr (insertl o f) xs []"
-  by pat_completeness auto
-termination map_distinct by (auto_term "{}")
+by pat_completeness auto
+termination by lexicographic_order
+
 lemmas map_distinct_def = map_distinct.simps(2)
 declare map_distinct.simps[code]
 
@@ -133,8 +137,9 @@
 where
   "unions [] = []"
   "unions xs = foldr unionl xs []"
-  by pat_completeness auto
-termination unions by (auto_term "{}")
+by pat_completeness auto
+termination by lexicographic_order
+
 lemmas unions_def = unions.simps(2)
 declare unions.simps[code]