equal
deleted
inserted
replaced
363 | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; |
363 | mk_ctupleT Ts = foldr1 HOLogic.mk_prodT Ts; |
364 fun mk_maybeT T = Type ("Fixrec.maybe",[T]); |
364 fun mk_maybeT T = Type ("Fixrec.maybe",[T]); |
365 fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; |
365 fun cpair_pat (p1,p2) = %%: @{const_name cpair_pat} $ p1 $ p2; |
366 val mk_ctuple_pat = foldr1 cpair_pat; |
366 val mk_ctuple_pat = foldr1 cpair_pat; |
367 fun lift_defined f = lift (fn x => defined (f x)); |
367 fun lift_defined f = lift (fn x => defined (f x)); |
368 fun bound_arg vns v = Bound(length vns -find_index_eq v vns -1); |
368 fun bound_arg vns v = Bound (length vns - find_index (fn v' => v' = v) vns - 1); |
369 |
369 |
370 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = |
370 fun cont_eta_contract (Const("Cfun.Abs_CFun",TT) $ Abs(a,T,body)) = |
371 (case cont_eta_contract body of |
371 (case cont_eta_contract body of |
372 body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => |
372 body' as (Const("Cfun.Rep_CFun",Ta) $ f $ Bound 0) => |
373 if not (0 mem loose_bnos f) then incr_boundvars ~1 f |
373 if not (0 mem loose_bnos f) then incr_boundvars ~1 f |