# HG changeset patch
# User wenzelm
# Date 1240695750 -7200
# Node ID 2a22c6613dcf150973f37531a8c03b782a8bd738
# Parent  e6349035148ab5041b31c0e01898869b0f10eca3
append prefs at end;

diff -r e6349035148a -r 2a22c6613dcf src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 22:29:13 2009 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 23:42:30 2009 +0200
@@ -204,6 +204,6 @@
     else
       if exists (fn {name, ...} => name = #name pref) prefs
       then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
-      else (cat, pref :: prefs));
+      else (cat, prefs @ [pref]));
 
 end;