append prefs at end;
authorwenzelm
Sat, 25 Apr 2009 23:42:30 +0200
changeset 30985 2a22c6613dcf
parent 30984 e6349035148a
child 30987 2bbc22bd6a95
append prefs at end;
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;