89 val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)" |
89 val SOME t = parseNEW ctxt "1 = 2 * (1 + -1 * sqrt x)" |
90 val SOME (t, _) = rewrite_set_ thy true make_rooteq t; |
90 val SOME (t, _) = rewrite_set_ thy true make_rooteq t; |
91 term2str t = "1 = 2 + -2 * sqrt x"; |
91 term2str t = "1 = 2 + -2 * sqrt x"; |
92 (*... which works; thus error must be in script interpretation*) |
92 (*... which works; thus error must be in script interpretation*) |
93 |
93 |
94 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
94 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); |
95 val (pt, p) = case locatetac tac (pt,p) of |
95 val (pt, p) = case locatetac tac (pt,p) of |
96 ("ok", (_, _, ptp)) => ptp; |
96 ("ok", (_, _, ptp)) => ptp; |
97 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
97 "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), [])) |
98 val pIopt = get_pblID (pt,ip); |
98 val pIopt = get_pblID (pt,ip); |
99 ip; (*= ([3, 2], Res)*) |
99 ip; (*= ([3, 2], Res)*) |