src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 47433 07f4bf913230
parent 46115 ecab67f5a5c2
child 47753 792634c6679e
equal deleted inserted replaced
47306:56d72c923281 47433:07f4bf913230
   520         | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
   520         | (Const (@{const_name Id}, T), []) => Cst (Iden, T, Any)
   521         | (Const (@{const_name converse}, T), [t1]) =>
   521         | (Const (@{const_name converse}, T), [t1]) =>
   522           Op1 (Converse, range_type T, Any, sub t1)
   522           Op1 (Converse, range_type T, Any, sub t1)
   523         | (Const (@{const_name trancl}, T), [t1]) =>
   523         | (Const (@{const_name trancl}, T), [t1]) =>
   524           Op1 (Closure, range_type T, Any, sub t1)
   524           Op1 (Closure, range_type T, Any, sub t1)
   525         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   525         | (Const (@{const_name relcomp}, T), [t1, t2]) =>
   526           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   526           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   527         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   527         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   528           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   528           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   529           else if is_constr ctxt stds x then do_construct x []
   529           else if is_constr ctxt stds x then do_construct x []
   530           else ConstName (s, T, Any)
   530           else ConstName (s, T, Any)