equal
deleted
inserted
replaced
148 struct |
148 struct |
149 |
149 |
150 local |
150 local |
151 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); |
151 fun lhs_of eq = fst (Thm.dest_equals (cprop_of eq)); |
152 in |
152 in |
153 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", []) |
153 fun rewrite_conv [] ct = raise CTERM ("rewrite_conv", [ct]) |
154 | rewrite_conv (eq :: eqs) ct = |
154 | rewrite_conv (eq :: eqs) ct = |
155 Thm.instantiate (Thm.match (lhs_of eq, ct)) eq |
155 Thm.instantiate (Thm.match (lhs_of eq, ct)) eq |
156 handle Pattern.MATCH => rewrite_conv eqs ct; |
156 handle Pattern.MATCH => rewrite_conv eqs ct; |
157 end |
157 end |
158 |
158 |