equal
deleted
inserted
replaced
207 val it = "x + #1 = #2" : string *) |
207 val it = "x + #1 = #2" : string *) |
208 |
208 |
209 |
209 |
210 (*.get argument of first stactic in a script for init_form.*) |
210 (*.get argument of first stactic in a script for init_form.*) |
211 fun get_stac thy (h $ body) = |
211 fun get_stac thy (h $ body) = |
|
212 (* |
|
213 *) |
212 let |
214 let |
213 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = |
215 fun get_t y (Const ("Script.Seq",_) $ e1 $ e2) a = |
214 (case get_t y e1 a of None => get_t y e2 a | la => la) |
216 (case get_t y e1 a of None => get_t y e2 a | la => la) |
215 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = |
217 | get_t y (Const ("Script.Seq",_) $ e1 $ e2 $ a) _ = |
216 (case get_t y e1 a of None => get_t y e2 a | la => la) |
218 (case get_t y e1 a of None => get_t y e2 a | la => la) |