equal
deleted
inserted
replaced
167 |
167 |
168 fun iso_tuple_intros_tac ctxt = |
168 fun iso_tuple_intros_tac ctxt = |
169 resolve_from_net_tac ctxt iso_tuple_intros THEN' |
169 resolve_from_net_tac ctxt iso_tuple_intros THEN' |
170 CSUBGOAL (fn (cgoal, i) => |
170 CSUBGOAL (fn (cgoal, i) => |
171 let |
171 let |
172 val thy = Thm.theory_of_cterm cgoal; |
|
173 val goal = Thm.term_of cgoal; |
172 val goal = Thm.term_of cgoal; |
174 |
173 |
175 val isthms = Iso_Tuple_Thms.get thy; |
174 val isthms = Iso_Tuple_Thms.get (Proof_Context.theory_of ctxt); |
176 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]); |
175 fun err s t = raise TERM ("iso_tuple_intros_tac: " ^ s, [t]); |
177 |
176 |
178 val goal' = Envir.beta_eta_contract goal; |
177 val goal' = Envir.beta_eta_contract goal; |
179 val is = |
178 val is = |
180 (case goal' of |
179 (case goal' of |