src/HOL/Tools/Nitpick/nitpick_preproc.ML
changeset 35190 ce653cc27a94
parent 35187 3acab6c90d4a
child 35220 2bcdae5f4fdb
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 14:11:41 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Feb 17 20:46:50 2010 +0100
     1.3 @@ -9,7 +9,8 @@
     1.4  sig
     1.5    type hol_context = Nitpick_HOL.hol_context
     1.6    val preprocess_term :
     1.7 -    hol_context -> term -> ((term list * term list) * (bool * bool)) * term
     1.8 +    hol_context -> term
     1.9 +    -> ((term list * term list) * (bool * bool)) * term * bool
    1.10  end
    1.11  
    1.12  structure Nitpick_Preproc : NITPICK_PREPROC =
    1.13 @@ -54,15 +55,6 @@
    1.14    | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
    1.15    | should_use_binary_ints _ = false
    1.16  
    1.17 -(* typ -> typ *)
    1.18 -fun binarize_nat_and_int_in_type @{typ nat} = @{typ "unsigned_bit word"}
    1.19 -  | binarize_nat_and_int_in_type @{typ int} = @{typ "signed_bit word"}
    1.20 -  | binarize_nat_and_int_in_type (Type (s, Ts)) =
    1.21 -    Type (s, map binarize_nat_and_int_in_type Ts)
    1.22 -  | binarize_nat_and_int_in_type T = T
    1.23 -(* term -> term *)
    1.24 -val binarize_nat_and_int_in_term = map_types binarize_nat_and_int_in_type
    1.25 -
    1.26  (** Uncurrying **)
    1.27  
    1.28  (* theory -> term -> int Termtab.tab -> int Termtab.tab *)
    1.29 @@ -1383,7 +1375,8 @@
    1.30  
    1.31  (** Preprocessor entry point **)
    1.32  
    1.33 -(* hol_context -> term -> ((term list * term list) * (bool * bool)) * term *)
    1.34 +(* hol_context -> term
    1.35 +   -> ((term list * term list) * (bool * bool)) * term * bool *)
    1.36  fun preprocess_term (hol_ctxt as {thy, binary_ints, destroy_constrs, boxes,
    1.37                                    skolemize, uncurry, ...}) t =
    1.38    let
    1.39 @@ -1424,7 +1417,7 @@
    1.40    in
    1.41      (((map (do_rest true false) def_ts, map (do_rest false false) nondef_ts),
    1.42        (got_all_mono_user_axioms, no_poly_user_axioms)),
    1.43 -     do_rest false true core_t)
    1.44 +     do_rest false true core_t, binarize)
    1.45    end
    1.46  
    1.47  end;