1209 (*Conversion to apply the meta simpset to a term*) |
1209 (*Conversion to apply the meta simpset to a term*) |
1210 fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = |
1210 fun rewritec (prover,signt) (mss as Mss{net,...}) (hypst,t) = |
1211 let val t = Pattern.eta_contract t; |
1211 let val t = Pattern.eta_contract t; |
1212 fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = |
1212 fun rew {thm as Thm{sign,hyps,maxidx,prop,...}, lhs, perm} = |
1213 let val unit = if Sign.subsig(sign,signt) then () |
1213 let val unit = if Sign.subsig(sign,signt) then () |
1214 else (writeln"Warning: rewrite rule from different theory"; |
1214 else (trace_thm"Warning: rewrite rule from different theory" |
|
1215 thm; |
1215 raise Pattern.MATCH) |
1216 raise Pattern.MATCH) |
1216 val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t) |
1217 val insts = Pattern.match (#tsig(Sign.rep_sg signt)) (lhs,t) |
1217 val prop' = subst_vars insts prop; |
1218 val prop' = subst_vars insts prop; |
1218 val hyps' = hyps union hypst; |
1219 val hyps' = hyps union hypst; |
1219 val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} |
1220 val thm' = Thm{sign=signt, hyps=hyps', prop=prop', maxidx=maxidx} |