11 (*for resuming after stepping into code*) |
11 (*for resuming after stepping into code*) |
12 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt); |
12 val (p''',f''',nxt''',pt''') = (p,f,nxt,pt); |
13 |
13 |
14 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt); |
14 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), (_:NEW), (pt:ctree)) = (nxt, p, [], pt); |
15 val (pt, p) = |
15 val (pt, p) = |
|
16 (*ERROR nxt_add: types or dsc DO NOT MATCH BETWEEN fmz --- pbt ... see 100-init-rootpbl.sml*) |
16 case locatetac tac (pt,p) of |
17 case locatetac tac (pt,p) of |
17 ("ok", (_, _, ptp)) => ptp; |
18 ("ok", (_, _, ptp)) => ptp; |
18 (* val (_, ts) = |
19 (* val (_, ts) = |
19 (case step p ((pt, e_pos'),[]) of |
20 (case step p ((pt, e_pos'),[]) of |
20 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)) |
21 ("ok", (ts as (tac,_,_)::_, _, _)) => ("",ts)) |