append prefs at end;
authorwenzelm
Sat, 25 Apr 2009 23:42:30 +0200
changeset 309852a22c6613dcf
parent 30984 e6349035148a
child 30987 2bbc22bd6a95
append prefs at end;
src/Pure/ProofGeneral/preferences.ML
     1.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 22:29:13 2009 +0200
     1.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 25 23:42:30 2009 +0200
     1.3 @@ -204,6 +204,6 @@
     1.4      else
     1.5        if exists (fn {name, ...} => name = #name pref) prefs
     1.6        then (warning ("Preference already exists: " ^ quote (#name pref)); (cat, prefs))
     1.7 -      else (cat, pref :: prefs));
     1.8 +      else (cat, prefs @ [pref]));
     1.9  
    1.10  end;