equal
deleted
inserted
replaced
161 |
161 |
162 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
162 fun dest_fsetT (Type (@{type_name fset}, [T])) = T |
163 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
163 | dest_fsetT T = raise TYPE ("dest_fsetT: fset type expected", [T], []); |
164 |
164 |
165 |
165 |
166 |
166 fun mk_id trm = HOLogic.id_const (fastype_of trm) $ trm |
167 fun mk_id trm = |
|
168 let |
|
169 val ty = fastype_of trm |
|
170 in |
|
171 Const (@{const_name id}, ty --> ty) $ trm |
|
172 end |
|
173 |
167 |
174 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
168 fun mk_all (a, T) t = Term.all T $ Abs (a, T, t) |
175 |
169 |
176 fun sum_case_const ty1 ty2 ty3 = |
170 fun sum_case_const ty1 ty2 ty3 = |
177 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |
171 Const (@{const_name sum_case}, [ty1 --> ty3, ty2 --> ty3, Type (@{type_name sum}, [ty1, ty2])] ---> ty3) |