# HG changeset patch
# User bulwahn
# Date 1282824431 -7200
# Node ID 499135eb21ec5698a343a3c55ca1d90105f35834
# Parent  d171840881fddd0fb537009f154e635da6cd228d
moving options; tuned

diff -r d171840881fd -r 499135eb21ec src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 13:49:12 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 14:07:11 2010 +0200
@@ -230,28 +230,6 @@
       in clause end
   in (map translate_intro intros', constant_table') end
 
-val preprocess_options = Predicate_Compile_Aux.Options {
-  expected_modes = NONE,
-  proposed_modes = NONE,
-  proposed_names = [],
-  show_steps = false,
-  show_intermediate_results = false,
-  show_proof_trace = false,
-  show_modes = false,
-  show_mode_inference = false,
-  show_compilation = false,
-  show_caught_failures = false,
-  skip_proof = true,
-  no_topmost_reordering = false,
-  function_flattening = true,
-  specialise = false,
-  fail_safe_function_flattening = false,
-  no_higher_order_predicate = [],
-  inductify = false,
-  detect_switches = true,
-  compilation = Predicate_Compile_Aux.Pred
-}
-
 fun depending_preds_of (key, intros) =
   fold Term.add_const_names (map Thm.prop_of intros) []
 
@@ -422,7 +400,7 @@
 fun write_program p =
   cat_lines (map write_clause p) 
 
-(** query templates **)
+(* query templates *)
 
 fun query_first rel vnames =
   "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
@@ -447,6 +425,7 @@
   "main :- halt(1).\n"
 
 (* parsing prolog solution *)
+
 val scan_number =
   Scan.many1 Symbol.is_ascii_digit
 
@@ -516,7 +495,7 @@
     tss
   end
 
-(* values command *)
+(* restoring types in terms *)
 
 fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
   | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
@@ -535,6 +514,30 @@
         map (restore_term ctxt constant_table) (args ~~ argsT'))
     end
 
+(* values command *)
+
+val preprocess_options = Predicate_Compile_Aux.Options {
+  expected_modes = NONE,
+  proposed_modes = NONE,
+  proposed_names = [],
+  show_steps = false,
+  show_intermediate_results = false,
+  show_proof_trace = false,
+  show_modes = false,
+  show_mode_inference = false,
+  show_compilation = false,
+  show_caught_failures = false,
+  skip_proof = true,
+  no_topmost_reordering = false,
+  function_flattening = true,
+  specialise = false,
+  fail_safe_function_flattening = false,
+  no_higher_order_predicate = [],
+  inductify = false,
+  detect_switches = true,
+  compilation = Predicate_Compile_Aux.Pred
+}
+
 fun values ctxt soln t_compr =
   let
     val options = !options