# HG changeset patch
# User bulwahn
# Date 1267108598 -3600
# Node ID 5038f36b5ea17dd19766910e2f863cab3d7daaab
# Parent  6ac5b81a763d719ccff13ef2447244f646d17949
adding no_topmost_reordering as new option to the code_pred command

diff -r 6ac5b81a763d -r 5038f36b5ea1 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 25 14:01:34 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Thu Feb 25 15:36:38 2010 +0100
@@ -151,7 +151,7 @@
       skip_proof = chk "skip_proof",
       function_flattening = not (chk "no_function_flattening"),
       fail_safe_function_flattening = false,
-      no_topmost_reordering = false,
+      no_topmost_reordering = (chk "no_topmost_reordering"),
       no_higher_order_predicate = [],
       inductify = chk "inductify",
       compilation = compilation
diff -r 6ac5b81a763d -r 5038f36b5ea1 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 25 14:01:34 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Feb 25 15:36:38 2010 +0100
@@ -556,7 +556,8 @@
 }
 
 val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", "show_modes",
-  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening"]
+  "show_mode_inference", "show_compilation", "skip_proof", "inductify", "no_function_flattening",
+  "no_topmost_reordering"]
 
 val compilation_names = [("pred", Pred),
   (*("random", Random), ("depth_limited", Depth_Limited), ("annotated", Annotated),*)