1.1 --- a/src/Tools/isac/Interpret/solve.sml	Wed Oct 06 14:52:12 2010 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Wed Oct 06 15:12:41 2010 +0200
     1.3 @@ -173,7 +173,7 @@
     1.4  		  ("ok", (map step2taci ss, c', (pt',p')))
     1.5  		| NotLocatable =>  
     1.6  		  let val (p,ps,f,pt) = 
     1.7 -			  generate_hard (assoc_thy "Isac.thy") m (p,Frm) pt;
     1.8 +			  generate_hard (assoc_thy "Isac") m (p,Frm) pt;
     1.9  		  in ("not-found-in-script",
    1.10  		      ([(tac_2tac m, m, (pos, is))], ps, (pt,p))) end
    1.11      (*just-before------------------------------------------------------
    1.12 @@ -307,7 +307,7 @@
    1.13  		   map step2taci ss, c', (pt',p'))) end
    1.14  	     | NotLocatable =>  
    1.15  	       let val (p,ps,f,pt) = 
    1.16 -		       generate_hard (assoc_thy "Isac.thy") m (p,p_) pt;
    1.17 +		       generate_hard (assoc_thy "Isac") m (p,p_) pt;
    1.18  	       in ("not-found-in-script",
    1.19  		   ((*(p,Uistate,Empty_Tac_),f, Empty_Tac, Unsafe,*) 
    1.20  		   [(tac_2tac m, m, (po,is))], ps, (pt,p))) end
    1.21 @@ -424,7 +424,7 @@
    1.22  		    | _ => pos  (*somewhere in script*)
    1.23      (*val _= tracing"### nxt_solv4 Apply_Method: stored is =";
    1.24          val _= tracing(istate2str is);*)
    1.25 -	val (pos',c,_,pt) = generate1 (assoc_thy "Isac.thy") tac_ is pos pt;
    1.26 +	val (pos',c,_,pt) = generate1 (assoc_thy "Isac") tac_ is pos pt;
    1.27      in ([(tac_2tac tac_, tac_, (pos,is))], c, (pt, pos')) end
    1.28  
    1.29  
    1.30 @@ -564,7 +564,7 @@
    1.31  	       val tac_ = Apply_Method' (e_metID(*WN0402: see generate1 !?!*), 
    1.32  					 SOME t, is)
    1.33  	       val pos' = ((lev_on o lev_dn) p, Frm)
    1.34 -	       val thy = assoc_thy "Isac.thy"
    1.35 +	       val thy = assoc_thy "Isac"
    1.36  	       val (_,_,_,pt') = (*implicit Take*)generate1 thy tac_ is pos' pt
    1.37  	       val (_,_,(pt'',_)) = complete_solve CompleteSubpbl [] (pt',pos')
    1.38  	       val newnds = children (get_nd pt'' p)