1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:06 2010 +0200
     1.3 @@ -297,14 +297,14 @@
     1.4  
     1.5  (* diagnostic display functions *)
     1.6  
     1.7 -fun print_modes options thy modes =
     1.8 +fun print_modes options modes =
     1.9    if show_modes options then
    1.10      tracing ("Inferred modes:\n" ^
    1.11        cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
    1.12          (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
    1.13    else ()
    1.14  
    1.15 -fun print_pred_mode_table string_of_entry thy pred_mode_table =
    1.16 +fun print_pred_mode_table string_of_entry pred_mode_table =
    1.17    let
    1.18      fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
    1.19        ^ string_of_entry pred mode entry
    1.20 @@ -2832,7 +2832,7 @@
    1.21      val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
    1.22      val _ = check_expected_modes preds options modes
    1.23      (*val _ = check_proposed_modes preds options modes (fst extra_modes) errors*)
    1.24 -    val _ = print_modes options thy' modes
    1.25 +    val _ = print_modes options modes
    1.26      val _ = print_step options "Defining executable functions..."
    1.27      val thy'' =
    1.28        Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."