test/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 41973 bf17547ce960
parent 41972 22c5483e9bfb
child 41982 90f65f1b6351
     1.1 --- a/test/Tools/isac/Interpret/script.sml	Wed May 04 09:01:10 2011 +0200
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Wed May 04 14:04:53 2011 +0200
     1.3 @@ -303,10 +303,8 @@
     1.4  (*val (p,_,f,nxt,_,pt) = me nxt p [1] pt; WAS: Empty_Tac, helpless*)
     1.5  show_pt pt;
     1.6  "~~~~~ fun me, args:"; val (_,tac) = nxt;
     1.7 -    val (pt, p) = 
     1.8 -	    (*locatetac is here for testing by me; step would suffice in me*)
     1.9 -	    case locatetac tac (pt,p) of
    1.10 -		      ("ok", (_, _, ptp))  => ptp | _ => error "test";
    1.11 +val (pt, p) = case locatetac tac (pt,p) of
    1.12 +	("ok", (_, _, ptp))  => ptp | _ => error "script.sml locatetac";
    1.13  "~~~~~ fun step, args:"; val (ip as (_,p_), (ptp as (pt,p), tacis)) = (p, ((pt, e_pos'), []))
    1.14  val pIopt = get_pblID (pt,ip);
    1.15  tacis; (*= []*)