Lines Matching defs:M1
198 let val (J, M1, M2) = dest_cond M
199 val M1' = mk_flat_let (v, trav M1, N')
201 in mk_cond (J, M1', M2') end
206 let val (M1,M2) = dest_comb t
207 val M1' = trav M1
209 in mk_comb(M1',M2')
249 let val (J, M1, M2) = dest_cond M
250 val M1' = mk_plet (v, lift_cond M1, N')
259 val t2 = rhs (concl (SPECL [f, J, M1, M2] th))