equal
deleted
inserted
replaced
75 (*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*) |
75 (*stolen from ~~/src/HOL/Tools/Nitpick/nitpick_hol.ML*) |
76 fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T |
76 fun num_binder_types (Type (@{type_name fun}, [_, T])) = 1 + num_binder_types T |
77 | num_binder_types _ = 0; |
77 | num_binder_types _ = 0; |
78 |
78 |
79 val exists_subtype_in = Term.exists_subtype o member (op =); |
79 val exists_subtype_in = Term.exists_subtype o member (op =); |
80 fun exists_strict_subtype_in Ts T = exists_subtype_in (filter_out (curry (op =) T) Ts) T; |
80 fun exists_strict_subtype_in Ts T = exists_subtype_in (remove (op =) T Ts) T; |
81 |
81 |
82 fun tvar_subst thy Ts Us = |
82 fun tvar_subst thy Ts Us = |
83 Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; |
83 Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; |
84 |
84 |
85 fun retype_const_or_free T (Const (s, _)) = Const (s, T) |
85 fun retype_const_or_free T (Const (s, _)) = Const (s, T) |