equal
deleted
inserted
replaced
205 | mk_ctuple ts = foldr1 cpair ts; |
205 | mk_ctuple ts = foldr1 cpair ts; |
206 fun mk_stuple [] = %%:ONE_N |
206 fun mk_stuple [] = %%:ONE_N |
207 | mk_stuple ts = foldr1 spair ts; |
207 | mk_stuple ts = foldr1 spair ts; |
208 fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) |
208 fun mk_ctupleT [] = HOLogic.unitT (* used in match_defs *) |
209 | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; |
209 | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; |
|
210 fun mk_maybeT T = Type ("Fixrec.maybe",[T]); |
210 fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2; |
211 fun cpair_pat (p1,p2) = %%:cpair_patN $ p1 $ p2; |
211 fun lift_defined f = lift (fn x => defined (f x)); |
212 fun lift_defined f = lift (fn x => defined (f x)); |
212 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); |
213 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); |
213 |
214 |
214 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = |
215 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = |