61 fun register_n2m_sugar key n2m_sugar = |
61 fun register_n2m_sugar key n2m_sugar = |
62 Local_Theory.declaration {syntax = false, pervasive = false} |
62 Local_Theory.declaration {syntax = false, pervasive = false} |
63 (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar))); |
63 (fn phi => Data.map (Typtab.default (key, morph_n2m_sugar phi n2m_sugar))); |
64 |
64 |
65 fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1)) |
65 fun unfold_let (Const (@{const_name Let}, _) $ arg1 $ arg2) = unfold_let (betapply (arg2, arg1)) |
66 | unfold_let (Const (@{const_name prod_case}, _) $ t) = |
66 | unfold_let (t as Const (@{const_name prod_case}, _) $ u) = |
67 (case unfold_let t of |
67 (case unfold_let u of |
68 t' as Abs (s1, T1, Abs (s2, T2, _)) => |
68 u' as Abs (s1, T1, Abs (s2, T2, _)) => |
69 let val v = Var ((s1 ^ s2, Term.maxidx_of_term t' + 1), HOLogic.mk_prodT (T1, T2)) in |
69 let val v = Var ((s1 ^ s2, Term.maxidx_of_term u' + 1), HOLogic.mk_prodT (T1, T2)) in |
70 lambda v (incr_boundvars 1 (betapplys (t', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) |
70 lambda v (incr_boundvars 1 (betapplys (u', [HOLogic.mk_fst v, HOLogic.mk_snd v]))) |
71 end |
71 end |
72 | _ => t) |
72 | _ => t) |
73 | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u) |
73 | unfold_let (t $ u) = betapply (unfold_let t, unfold_let u) |
74 | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t) |
74 | unfold_let (Abs (s, T, t)) = Abs (s, T, unfold_let t) |
75 | unfold_let t = t; |
75 | unfold_let t = t; |