# HG changeset patch
# User bulwahn
# Date 1288034233 -7200
# Node ID 432a776c4aee2e03b0a31a773330f8d3060c9b17
# Parent  9eabcb1bfe509c077ec32faf37ca628a1aa569a9
options as first argument to check functions

diff -r 9eabcb1bfe50 -r 432a776c4aee src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Oct 25 21:17:13 2010 +0200
@@ -167,7 +167,7 @@
 
 (* validity checks *)
 
-fun check_expected_modes preds options modes =
+fun check_expected_modes options preds modes =
   case expected_modes options of
     SOME (s, ms) => (case AList.lookup (op =) modes s of
       SOME modes =>
@@ -183,7 +183,7 @@
       | NONE => ())
   | NONE => ()
 
-fun check_proposed_modes preds options modes errors =
+fun check_proposed_modes options preds modes errors =
   map (fn (s, _) => case proposed_modes options s of
     SOME ms => (case AList.lookup (op =) modes s of
       SOME inferred_ms =>
@@ -1379,8 +1379,8 @@
         options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
     val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random 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 errors
+    val _ = check_expected_modes options preds modes
+    val _ = check_proposed_modes options preds modes errors
     val _ = print_modes options modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =