equal
deleted
inserted
replaced
101 map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}] |
101 map (fn c => c RS eq_reflection) [@{thm "cong"}, @{thm "ext"}] |
102 |
102 |
103 (* Called on the INSTANTIATED branches of the congruence rule *) |
103 (* Called on the INSTANTIATED branches of the congruence rule *) |
104 fun mk_branch ctxt t = |
104 fun mk_branch ctxt t = |
105 let |
105 let |
106 val ((fixes, impl), ctxt') = Function_Lib.focus_term t ctxt |
106 val ((params, impl), ctxt') = Variable.focus t ctxt |
107 val (assms, concl) = Logic.strip_horn impl |
107 val (assms, concl) = Logic.strip_horn impl |
108 in |
108 in |
109 (ctxt', fixes, assms, rhs_of concl) |
109 (ctxt', map #2 params, assms, rhs_of concl) |
110 end |
110 end |
111 |
111 |
112 fun find_cong_rule ctxt fvar h ((r,dep)::rs) t = |
112 fun find_cong_rule ctxt fvar h ((r,dep)::rs) t = |
113 (let |
113 (let |
114 val thy = Proof_Context.theory_of ctxt |
114 val thy = Proof_Context.theory_of ctxt |