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 ((params, impl), ctxt') = Variable.focus t ctxt |
106 val ((params, impl), ctxt') = Variable.focus NONE t ctxt |
107 val (assms, concl) = Logic.strip_horn impl |
107 val (assms, concl) = Logic.strip_horn impl |
108 in |
108 in |
109 (ctxt', map #2 params, assms, rhs_of concl) |
109 (ctxt', map #2 params, assms, rhs_of concl) |
110 end |
110 end |
111 |
111 |