# HG changeset patch
# User bulwahn
# Date 1274286246 -7200
# Node ID c62f743e37d4987b584757a7df871c3c1371caa9
# Parent  a393a588b82ecc91a32294c43ad2de544012d9e0
removing unused argument in print_modes function

diff -r a393a588b82e -r c62f743e37d4 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:05 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:06 2010 +0200
@@ -297,14 +297,14 @@
 
 (* diagnostic display functions *)
 
-fun print_modes options thy modes =
+fun print_modes options modes =
   if show_modes options then
     tracing ("Inferred modes:\n" ^
       cat_lines (map (fn (s, ms) => s ^ ": " ^ commas (map
         (fn (p, m) => string_of_mode m ^ (if p then "pos" else "neg")) ms)) modes))
   else ()
 
-fun print_pred_mode_table string_of_entry thy pred_mode_table =
+fun print_pred_mode_table string_of_entry pred_mode_table =
   let
     fun print_mode pred ((pol, mode), entry) =  "mode : " ^ string_of_mode mode
       ^ string_of_entry pred mode entry
@@ -2832,7 +2832,7 @@
     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 _ = print_modes options thy' modes
+    val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =
       Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."