src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 41046 f2e94005d283
parent 39360 cdf2c3341422
child 41047 9f1d3fcef1ca
equal deleted inserted replaced
41045:2a41709f34c1 41046:f2e94005d283
   526           Op1 (Converse, range_type T, Any, sub t1)
   526           Op1 (Converse, range_type T, Any, sub t1)
   527         | (Const (@{const_name trancl}, T), [t1]) =>
   527         | (Const (@{const_name trancl}, T), [t1]) =>
   528           Op1 (Closure, range_type T, Any, sub t1)
   528           Op1 (Closure, range_type T, Any, sub t1)
   529         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   529         | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
   530           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   530           Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
   531         | (Const (@{const_name Sigma}, T), [t1, Abs (s, T', t2')]) =>
   531         | (Const (@{const_name prod}, T), [t1, t2]) =>
   532           Op2 (Product, nth_range_type 2 T, Any, sub t1, sub_abs s T' t2')
   532           Op2 (Product, nth_range_type 2 T, Any, sub t1, sub t2)
   533         | (Const (@{const_name image}, T), [t1, t2]) =>
   533         | (Const (@{const_name image}, T), [t1, t2]) =>
   534           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
   534           Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
   535         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   535         | (Const (x as (s as @{const_name Suc}, T)), []) =>
   536           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   536           if is_built_in_const thy stds x then Cst (Suc, T, Any)
   537           else if is_constr ctxt stds x then do_construct x []
   537           else if is_constr ctxt stds x then do_construct x []