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) |