1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 13:49:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Aug 26 14:07:11 2010 +0200
     1.3 @@ -230,28 +230,6 @@
     1.4        in clause end
     1.5    in (map translate_intro intros', constant_table') end
     1.6  
     1.7 -val preprocess_options = Predicate_Compile_Aux.Options {
     1.8 -  expected_modes = NONE,
     1.9 -  proposed_modes = NONE,
    1.10 -  proposed_names = [],
    1.11 -  show_steps = false,
    1.12 -  show_intermediate_results = false,
    1.13 -  show_proof_trace = false,
    1.14 -  show_modes = false,
    1.15 -  show_mode_inference = false,
    1.16 -  show_compilation = false,
    1.17 -  show_caught_failures = false,
    1.18 -  skip_proof = true,
    1.19 -  no_topmost_reordering = false,
    1.20 -  function_flattening = true,
    1.21 -  specialise = false,
    1.22 -  fail_safe_function_flattening = false,
    1.23 -  no_higher_order_predicate = [],
    1.24 -  inductify = false,
    1.25 -  detect_switches = true,
    1.26 -  compilation = Predicate_Compile_Aux.Pred
    1.27 -}
    1.28 -
    1.29  fun depending_preds_of (key, intros) =
    1.30    fold Term.add_const_names (map Thm.prop_of intros) []
    1.31  
    1.32 @@ -422,7 +400,7 @@
    1.33  fun write_program p =
    1.34    cat_lines (map write_clause p) 
    1.35  
    1.36 -(** query templates **)
    1.37 +(* query templates *)
    1.38  
    1.39  fun query_first rel vnames =
    1.40    "eval :- once("  ^ rel ^ "(" ^ space_implode ", " vnames ^ ")),\n" ^
    1.41 @@ -447,6 +425,7 @@
    1.42    "main :- halt(1).\n"
    1.43  
    1.44  (* parsing prolog solution *)
    1.45 +
    1.46  val scan_number =
    1.47    Scan.many1 Symbol.is_ascii_digit
    1.48  
    1.49 @@ -516,7 +495,7 @@
    1.50      tss
    1.51    end
    1.52  
    1.53 -(* values command *)
    1.54 +(* restoring types in terms *)
    1.55  
    1.56  fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
    1.57    | restore_term ctxt constant_table (Number n, @{typ "int"}) = HOLogic.mk_number @{typ "int"} n
    1.58 @@ -535,6 +514,30 @@
    1.59          map (restore_term ctxt constant_table) (args ~~ argsT'))
    1.60      end
    1.61  
    1.62 +(* values command *)
    1.63 +
    1.64 +val preprocess_options = Predicate_Compile_Aux.Options {
    1.65 +  expected_modes = NONE,
    1.66 +  proposed_modes = NONE,
    1.67 +  proposed_names = [],
    1.68 +  show_steps = false,
    1.69 +  show_intermediate_results = false,
    1.70 +  show_proof_trace = false,
    1.71 +  show_modes = false,
    1.72 +  show_mode_inference = false,
    1.73 +  show_compilation = false,
    1.74 +  show_caught_failures = false,
    1.75 +  skip_proof = true,
    1.76 +  no_topmost_reordering = false,
    1.77 +  function_flattening = true,
    1.78 +  specialise = false,
    1.79 +  fail_safe_function_flattening = false,
    1.80 +  no_higher_order_predicate = [],
    1.81 +  inductify = false,
    1.82 +  detect_switches = true,
    1.83 +  compilation = Predicate_Compile_Aux.Pred
    1.84 +}
    1.85 +
    1.86  fun values ctxt soln t_compr =
    1.87    let
    1.88      val options = !options