equal
deleted
inserted
replaced
260 > subst_stacexpr [] NONE e_term t;*) |
260 > subst_stacexpr [] NONE e_term t;*) |
261 |
261 |
262 |
262 |
263 fun stacpbls (h $ body) = |
263 fun stacpbls (h $ body) = |
264 let |
264 let |
265 fun scan ts (Const ("Let",_) $ e $ (Abs (v,T,b))) = |
265 fun scan ts (Const ("HOL.Let",_) $ e $ (Abs (v,T,b))) = |
266 (scan ts e) @ (scan ts b) |
266 (scan ts e) @ (scan ts b) |
267 | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2) |
267 | scan ts (Const ("If",_) $ c $ e1 $ e2) = (scan ts e1) @ (scan ts e2) |
268 | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e |
268 | scan ts (Const ("Script.While",_) $ c $ e $ _) = scan ts e |
269 | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e |
269 | scan ts (Const ("Script.While",_) $ c $ e) = scan ts e |
270 | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e |
270 | scan ts (Const ("Script.Repeat",_) $ e $ _) = scan ts e |