equal
deleted
inserted
replaced
755 |
755 |
756 fun get_field_simps ctxt optcT t = |
756 fun get_field_simps ctxt optcT t = |
757 (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of |
757 (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of |
758 SOME (ths1, ths2, ths3, th4, th) => |
758 SOME (ths1, ths2, ths3, th4, th) => |
759 let val tr = |
759 let val tr = |
760 Thm.transfer (Proof_Context.theory_of ctxt) #> |
760 Thm.transfer' ctxt #> |
761 (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) |
761 (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm) |
762 in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end |
762 in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end |
763 | NONE => error "get_field_simps: lookup failed"); |
763 | NONE => error "get_field_simps: lookup failed"); |
764 |
764 |
765 fun nth_el_conv (_, _, _, nth_el_Cons, _) = |
765 fun nth_el_conv (_, _, _, nth_el_Cons, _) = |