1.1 --- a/src/sml/FE-interface/interface.sml Fri Jan 04 11:16:28 2008 +0100
1.2 +++ b/src/sml/FE-interface/interface.sml Fri Jan 04 16:08:52 2008 +0100
1.3 @@ -162,12 +162,13 @@
1.4
1.5 (*. apply a tactic at a position and update the calc-tree if applicable .*)
1.6 (* val (cI, ip, tac) = (1, p, hd appltacs);
1.7 + val (cI, ip, tac) = (1, p, (hd (sel_appl_atomic_tacs pt p)));
1.8 *)
1.9 fun applyTactic (cI:calcID) ip tac =
1.10 let val ((pt, _), _) = get_calc cI
1.11 val p = get_pos cI 1
1.12 in case locatetac tac (pt, ip) of
1.13 -(* val ("ok", (tacis, c, (_,p'))) = locatetac tac (pt, ip);
1.14 +(* val ("ok", (tacis, c, (pt',p'))) = locatetac tac (pt, ip);
1.15 *)
1.16 ("ok", (_, c, ptp as (_,p'))) =>
1.17 (upd_calc cI (ptp, []); upd_ipos cI 1 p';