diff -r 2dd23002c465 -r 6e9ab159512f src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Tue Jan 30 08:21:23 2007 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML	Tue Jan 30 13:14:41 2007 +0100
@@ -16,7 +16,13 @@
 			  get: unit -> string,
 			  set: string -> unit }
 
-  val preferences : (string * isa_preference list) list
+  (* table of categorised and preferences; names must be unique *)
+  type isa_preference_table = (string * isa_preference list) list
+
+  val preferences : isa_preference_table
+
+  val remove      : string -> isa_preference_table -> isa_preference_table
+  val set_default : string * string -> isa_preference_table -> isa_preference_table
 end
 
 structure Preferences : PREFERENCES =
@@ -151,4 +157,22 @@
      ("Tracing", tracing_preferences),
      ("Proof", proof_preferences)]
 
+type isa_preference_table = (string * isa_preference list) list
+
+fun remove name (preftable : isa_preference_table)  = 
+    map (fn (cat,prefs) => 
+	    (cat, filter_out (curry op= name o #name) prefs))
+        preftable;
+
+fun set_default (setname,newdefault) (preftable : isa_preference_table)  = 
+    map (fn (cat,prefs) => 
+	    (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
+			  => if (name = setname) then 
+				 (set newdefault;
+				  {name=name,descr=descr,default=newdefault,
+				  pgiptype=pgiptype,get=get,set=set})
+			     else pref)
+   		  prefs))
+        preftable;
+
 end