doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML
changeset 25182 64e3f45dc6f4
parent 24421 acfb2413faa3
child 25370 8b1aa4357320
--- a/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Oct 24 21:12:44 2007 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/examples/collect_duplicates.ML	Wed Oct 24 21:33:37 2007 +0200
@@ -17,11 +17,11 @@
 structure Codegen = 
 struct
 
-fun collect_duplicates B_ xs ys (z :: zs) =
-  (if List.member B_ z xs
-    then (if List.member B_ z ys then collect_duplicates B_ xs ys zs
-           else collect_duplicates B_ xs (z :: ys) zs)
-    else collect_duplicates B_ (z :: xs) (z :: ys) zs)
-  | collect_duplicates B_ xs ys [] = xs;
+fun collect_duplicates A_ xs ys (z :: zs) =
+  (if List.member A_ z xs
+    then (if List.member A_ z ys then collect_duplicates A_ xs ys zs
+           else collect_duplicates A_ xs (z :: ys) zs)
+    else collect_duplicates A_ (z :: xs) (z :: ys) zs)
+  | collect_duplicates A_ xs ys [] = xs;
 
 end; (*struct Codegen*)