using the proposed modes for starting the fixpoint iteration in the mode analysis

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 12:04:34 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 14:11:05 2010 +0200
@@ -379,7 +379,6 @@
   end
 
 (* validity checks *)
-(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)
 
 fun check_expected_modes preds options modes =
   case expected_modes options of
@@ -397,12 +396,12 @@
       | NONE => ())
   | NONE => ()
 
-fun check_proposed_modes preds options modes extra_modes errors =
+fun check_proposed_modes preds options modes errors =
   case proposed_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME inferred_ms =>
         let
-          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
+          val preds_without_modes = map fst (filter (null o snd) modes)
           val modes' = map snd inferred_ms
         in
           if not (eq_set eq_mode (ms, modes')) then
@@ -2695,12 +2694,16 @@
     val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
     val preds = map dest_Const preds
     val all_vs = terms_vs intrs
+    fun generate_modes s T =
+      if member (op =) (no_higher_order_predicate options) s then
+        all_smodes_of_typ T
+      else
+        all_modes_of_typ T
     val all_modes = 
       map (fn (s, T) =>
-        (s,
-            (if member (op =) (no_higher_order_predicate options) s then
-               (all_smodes_of_typ T)
-            else (all_modes_of_typ T)))) preds
+        (s, case (proposed_modes options) of
+            SOME (s', ms) => if s = s' then ms else generate_modes s T
+          | NONE => generate_modes s T)) preds
     val params =
       case intrs of
         [] =>
@@ -2848,7 +2851,7 @@
         options compilation preds all_modes param_vs clauses thy)
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
     val _ = check_expected_modes preds options modes
-    (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
+    val _ = check_proposed_modes preds options modes errors
     val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =