139 foldr1 HOLogic.mk_prodT Ts --> foldr1 HOLogic.mk_prodT Ts') $ t) Ts'; |
139 foldr1 HOLogic.mk_prodT Ts --> foldr1 HOLogic.mk_prodT Ts') $ t) Ts'; |
140 val projs = mk_proj (aux_lhs) Ts; |
140 val projs = mk_proj (aux_lhs) Ts; |
141 val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs; |
141 val proj_eqs = map2 (fn v => fn proj => (v, lambda arg proj)) vs projs; |
142 val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) => |
142 val proj_defs = map2 (fn Free (name, _) => fn (_, rhs) => |
143 ((Binding.concealed (Binding.name name), NoSyn), |
143 ((Binding.concealed (Binding.name name), NoSyn), |
144 (apfst Binding.concealed Attrib.empty_binding, rhs))) vs proj_eqs; |
144 (apfst Binding.concealed Binding.empty_atts, rhs))) vs proj_eqs; |
145 val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq; |
145 val aux_eq' = Pattern.rewrite_term thy proj_eqs [] aux_eq; |
146 fun prove_eqs aux_simp proj_defs lthy = |
146 fun prove_eqs aux_simp proj_defs lthy = |
147 let |
147 let |
148 val proj_simps = map (snd o snd) proj_defs; |
148 val proj_simps = map (snd o snd) proj_defs; |
149 fun tac { context = ctxt, prems = _ } = |
149 fun tac { context = ctxt, prems = _ } = |