1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 12:04:34 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Tue Sep 07 14:11:05 2010 +0200
     1.3 @@ -379,7 +379,6 @@
     1.4    end
     1.5  
     1.6  (* validity checks *)
     1.7 -(* EXPECTED MODE and PROPOSED_MODE are largely the same; define a clear semantics for those! *)
     1.8  
     1.9  fun check_expected_modes preds options modes =
    1.10    case expected_modes options of
    1.11 @@ -397,12 +396,12 @@
    1.12        | NONE => ())
    1.13    | NONE => ()
    1.14  
    1.15 -fun check_proposed_modes preds options modes extra_modes errors =
    1.16 +fun check_proposed_modes preds options modes errors =
    1.17    case proposed_modes options of
    1.18      SOME (s, ms) => (case AList.lookup (op =) modes s of
    1.19        SOME inferred_ms =>
    1.20          let
    1.21 -          val preds_without_modes = map fst (filter (null o snd) (modes @ extra_modes))
    1.22 +          val preds_without_modes = map fst (filter (null o snd) modes)
    1.23            val modes' = map snd inferred_ms
    1.24          in
    1.25            if not (eq_set eq_mode (ms, modes')) then
    1.26 @@ -2695,12 +2694,16 @@
    1.27      val ([preds, intrs], _) = fold_burrow (Variable.import_terms false) [preds, intrs] ctxt
    1.28      val preds = map dest_Const preds
    1.29      val all_vs = terms_vs intrs
    1.30 +    fun generate_modes s T =
    1.31 +      if member (op =) (no_higher_order_predicate options) s then
    1.32 +        all_smodes_of_typ T
    1.33 +      else
    1.34 +        all_modes_of_typ T
    1.35      val all_modes = 
    1.36        map (fn (s, T) =>
    1.37 -        (s,
    1.38 -            (if member (op =) (no_higher_order_predicate options) s then
    1.39 -               (all_smodes_of_typ T)
    1.40 -            else (all_modes_of_typ T)))) preds
    1.41 +        (s, case (proposed_modes options) of
    1.42 +            SOME (s', ms) => if s = s' then ms else generate_modes s T
    1.43 +          | NONE => generate_modes s T)) preds
    1.44      val params =
    1.45        case intrs of
    1.46          [] =>
    1.47 @@ -2848,7 +2851,7 @@
    1.48          options compilation preds all_modes param_vs clauses thy)
    1.49      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
    1.50      val _ = check_expected_modes preds options modes
    1.51 -    (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
    1.52 +    val _ = check_proposed_modes preds options modes errors
    1.53      val _ = print_modes options modes
    1.54      val _ = print_step options "Defining executable functions..."
    1.55      val thy'' =