src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 55888 cac1add157e8
parent 48323 7b5f7ca25d17
child 55889 6bfbec3dff62
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 16:44:46 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -418,7 +418,7 @@
     1.4      maps factorize [mk_fst z, mk_snd z]
     1.5    | factorize z = [z]
     1.6  
     1.7 -fun nut_from_term (hol_ctxt as {thy, ctxt, stds, ...}) eq =
     1.8 +fun nut_from_term (hol_ctxt as {ctxt, ...}) eq =
     1.9    let
    1.10      fun aux eq ss Ts t =
    1.11        let
    1.12 @@ -525,8 +525,8 @@
    1.13          | (Const (@{const_name relcomp}, T), [t1, t2]) =>
    1.14            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    1.15          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    1.16 -          if is_built_in_const thy stds x then Cst (Suc, T, Any)
    1.17 -          else if is_constr ctxt stds x then do_construct x []
    1.18 +          if is_built_in_const x then Cst (Suc, T, Any)
    1.19 +          else if is_constr ctxt x then do_construct x []
    1.20            else ConstName (s, T, Any)
    1.21          | (Const (@{const_name finite}, T), [t1]) =>
    1.22            (if is_finite_type hol_ctxt (domain_type T) then
    1.23 @@ -536,27 +536,27 @@
    1.24             | _ => Op1 (Finite, bool_T, Any, sub t1))
    1.25          | (Const (@{const_name nat}, T), []) => Cst (IntToNat, T, Any)
    1.26          | (Const (x as (s as @{const_name zero_class.zero}, T)), []) =>
    1.27 -          if is_built_in_const thy stds x then Cst (Num 0, T, Any)
    1.28 -          else if is_constr ctxt stds x then do_construct x []
    1.29 +          if is_built_in_const x then Cst (Num 0, T, Any)
    1.30 +          else if is_constr ctxt x then do_construct x []
    1.31            else ConstName (s, T, Any)
    1.32          | (Const (x as (s as @{const_name one_class.one}, T)), []) =>
    1.33 -          if is_built_in_const thy stds x then Cst (Num 1, T, Any)
    1.34 +          if is_built_in_const x then Cst (Num 1, T, Any)
    1.35            else ConstName (s, T, Any)
    1.36          | (Const (x as (s as @{const_name plus_class.plus}, T)), []) =>
    1.37 -          if is_built_in_const thy stds x then Cst (Add, T, Any)
    1.38 +          if is_built_in_const x then Cst (Add, T, Any)
    1.39            else ConstName (s, T, Any)
    1.40          | (Const (x as (s as @{const_name minus_class.minus}, T)), []) =>
    1.41 -          if is_built_in_const thy stds x then Cst (Subtract, T, Any)
    1.42 +          if is_built_in_const x then Cst (Subtract, T, Any)
    1.43            else ConstName (s, T, Any)
    1.44          | (Const (x as (s as @{const_name times_class.times}, T)), []) =>
    1.45 -          if is_built_in_const thy stds x then Cst (Multiply, T, Any)
    1.46 +          if is_built_in_const x then Cst (Multiply, T, Any)
    1.47            else ConstName (s, T, Any)
    1.48          | (Const (x as (s as @{const_name div_class.div}, T)), []) =>
    1.49 -          if is_built_in_const thy stds x then Cst (Divide, T, Any)
    1.50 +          if is_built_in_const x then Cst (Divide, T, Any)
    1.51            else ConstName (s, T, Any)
    1.52          | (t0 as Const (x as (@{const_name ord_class.less}, _)),
    1.53             ts as [t1, t2]) =>
    1.54 -          if is_built_in_const thy stds x then
    1.55 +          if is_built_in_const x then
    1.56              Op2 (Less, bool_T, Any, sub t1, sub t2)
    1.57            else
    1.58              do_apply t0 ts
    1.59 @@ -564,7 +564,7 @@
    1.60             ts as [t1, t2]) =>
    1.61            if is_set_like_type (domain_type T) then
    1.62              Op2 (Subset, bool_T, Any, sub t1, sub t2)
    1.63 -          else if is_built_in_const thy stds x then
    1.64 +          else if is_built_in_const x then
    1.65              (* FIXME: find out if this case is necessary *)
    1.66              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
    1.67            else
    1.68 @@ -572,7 +572,7 @@
    1.69          | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
    1.70          | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
    1.71          | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
    1.72 -          if is_built_in_const thy stds x then
    1.73 +          if is_built_in_const x then
    1.74              let val num_T = domain_type T in
    1.75                Op2 (Apply, num_T --> num_T, Any,
    1.76                     Cst (Subtract, num_T --> num_T --> num_T, Any),
    1.77 @@ -595,12 +595,12 @@
    1.78                    T as @{typ "unsigned_bit word => signed_bit word"}), []) =>
    1.79            Cst (NatToInt, T, Any)
    1.80          | (t0 as Const (x as (s, T)), ts) =>
    1.81 -          if is_constr ctxt stds x then
    1.82 +          if is_constr ctxt x then
    1.83              do_construct x ts
    1.84            else if String.isPrefix numeral_prefix s then
    1.85              Cst (Num (the (Int.fromString (unprefix numeral_prefix s))), T, Any)
    1.86            else
    1.87 -            (case arity_of_built_in_const thy stds x of
    1.88 +            (case arity_of_built_in_const x of
    1.89                 SOME n =>
    1.90                 (case n - length ts of
    1.91                    0 => raise TERM ("Nitpick_Nut.nut_from_term.aux", [t])