simplified preferences, removed obsolete operations;

--- a/src/Pure/ProofGeneral/preferences.ML	Mon May 13 22:00:19 2013 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Mon May 13 22:12:24 2013 +0200
@@ -18,19 +18,14 @@
     get: unit -> string,
     set: string -> unit}
   val options_pref: string -> string -> string -> preference
-  val generic_pref: ('a -> string) -> (string -> 'a) -> PgipTypes.pgiptype ->
-    'a Unsynchronized.ref -> string -> string -> preference
   val string_pref: string Unsynchronized.ref -> string -> string -> preference
   val real_pref: real Unsynchronized.ref -> string -> string -> preference
   val int_pref: int Unsynchronized.ref -> string -> string -> preference
-  val nat_pref: int Unsynchronized.ref -> string -> string -> preference
   val bool_pref: bool Unsynchronized.ref -> string -> string -> preference
   type T = (string * preference list) list
   val thm_depsN: string
   val pure_preferences: T
-  val remove: string -> T -> T
   val add: string -> preference -> T -> T
-  val set_default: string * string -> T -> T
 end
 
 structure Preferences: PREFERENCES =
@@ -95,9 +90,6 @@
   generic_pref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE, NONE))
     (PgipTypes.Pgipint (NONE, NONE));
 
-val nat_pref =
-  generic_pref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat;
-
 val bool_pref =
   generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
 
@@ -172,7 +164,7 @@
  [bool_pref Raw_Simplifier.simp_trace_default
     "trace-simplifier"
     "Trace simplification rules.",
-  nat_pref Raw_Simplifier.simp_trace_depth_limit_default
+  int_pref Raw_Simplifier.simp_trace_depth_limit_default
     "trace-simplifier-depth"
     "Trace simplifier depth limit.",
   bool_pref Pattern.trace_unify_fail
@@ -195,7 +187,7 @@
     "skip-proofs"
     "Skip over proofs",
   proof_pref,
-  nat_pref Multithreading.max_threads
+  int_pref Multithreading.max_threads
     "max-threads"
     "Maximum number of threads",
   parallel_proof_pref];
@@ -211,18 +203,6 @@
 
 type T = (string * preference list) list;
 
-fun remove name (tab: T) = tab |> map
-  (fn (cat, prefs) => (cat, filter_out (curry op = name o #name) prefs));
-
-fun set_default (setname, newdefault) (tab: T) = tab |> map
-  (fn (cat, prefs) =>
-    (cat, prefs |> 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)));
-
 fun add cname (pref: preference) (tab: T) = tab |> map
   (fn (cat, prefs) =>
     if cat <> cname then (cat, prefs)