src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

   in
     fold print (all_modes_of compilation ctxt) ()
   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
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>

           else ()
         end
       | 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
             error ("expected modes were not inferred:\n"
             ^ "  inferred modes for " ^ s ^ ": " ^ commas (map string_of_mode modes')  ^ "\n"

     val preds = map (fn c => Const (c, Sign.the_const_type thy c)) prednames
     val (preds, intrs) = unify_consts thy preds intrs
     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
         [] =>
           let
             val T = snd (hd preds)

       Output.cond_timeit (!Quickcheck.timing) "Infering modes"
       (fn _ => infer_modes mode_analysis_options
         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'' =
       Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
       (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'