src/HOL/Tools/Nitpick/nitpick_nut.ML
changeset 47433 07f4bf913230
parent 46115 ecab67f5a5c2
child 47753 792634c6679e
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 08:55:06 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Apr 03 17:26:30 2012 +0900
     1.3 @@ -522,7 +522,7 @@
     1.4            Op1 (Converse, range_type T, Any, sub t1)
     1.5          | (Const (@{const_name trancl}, T), [t1]) =>
     1.6            Op1 (Closure, range_type T, Any, sub t1)
     1.7 -        | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
     1.8 +        | (Const (@{const_name relcomp}, T), [t1, t2]) =>
     1.9            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    1.10          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    1.11            if is_built_in_const thy stds x then Cst (Suc, T, Any)