src/sml/FE-interface/interface.sml
branchstart-work-070517
changeset 275 fe39922392ff
parent 273 7cb662bd345d
     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';