1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed May 11 14:58:07 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Wed May 11 16:51:30 2011 +0200
     1.3 @@ -462,31 +462,29 @@
     1.4        pt) end
     1.5  
     1.6    | generate1 thy (Substitute' (subte, t, t')) l (p,p_) pt =
     1.7 -    let val (pt,c) = cappend_atomic pt p l t (Substitute (subte2sube subte)) 
     1.8 -	(t',[]) Complete;
     1.9 -  in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, 
    1.10 -				term2str t')), pt) 
    1.11 -    end
    1.12 +      let 
    1.13 +        val (pt,c) =
    1.14 +          cappend_atomic pt p l t (Substitute (subte2sube subte)) (t',[]) Complete;
    1.15 +        in ((p,Res), c, Form' (FormKF(~1,EdUndef,(length p), Nundef, term2str t')), pt) 
    1.16 +        end
    1.17  
    1.18    | generate1 thy (Tac_ (_,f,id,f')) l (p,p_) pt =
    1.19 -    let val (pt,c) = cappend_atomic pt p l (str2term f) 
    1.20 -				    (Tac id) (str2term f',[]) Complete;
    1.21 -  in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
    1.22 +      let
    1.23 +        val (pt,c) =
    1.24 +          cappend_atomic pt p l (str2term f) (Tac id) (str2term f',[]) Complete;
    1.25 +      in ((p,Res), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f')), pt)end
    1.26  
    1.27 -  | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, f)) 
    1.28 -	      l (p,p_) pt =
    1.29 -    let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
    1.30 -	val (pt,c) = cappend_problem pt p l (fmz_, (domID, pblID, metID))
    1.31 -				     (oris, (domID, pblID, metID), hdl);
    1.32 -	(*val pbl = init_pbl ((#ppc o get_pbt) pblID);
    1.33 -	val pt = update_pblppc pt p pbl;--------4.9.03->Model_Problem*)
    1.34 -	(*val _= tracing("### generate1: is([3],Frm)= "^
    1.35 -		       (istate2str (get_istate pt ([3],Frm))));*)
    1.36 -	val f = Syntax.string_of_term (thy2ctxt thy) f;
    1.37 -    in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.38 +  | generate1 thy (Subproblem' ((domID, pblID, metID), oris, hdl, fmz_, ctxt, f)) 
    1.39 +	  l (p,p_) pt =
    1.40 +      let (*val _=tracing("###generate1 Subproblem': pos= "^pos'2str (p,p_))*)
    1.41 +	      val (pt,c) =
    1.42 +          cappend_problem pt p l (fmz_, (domID, pblID, metID)) (oris, (domID, pblID, metID), hdl);
    1.43 +        val pt = update_ctxt pt (p, Res) ctxt (*FIXME.WN110511*)   
    1.44 +	      val f = Syntax.string_of_term (thy2ctxt thy) f;
    1.45 +      in ((p,Pbl), c, Form' (FormKF (~1,EdUndef,(length p), Nundef, f)), pt) end
    1.46  
    1.47    | generate1 thy m' _ _ _ = 
    1.48 -    error ("generate1: not impl.for "^(tac_2str m'))
    1.49 +      error ("generate1: not impl.for "^(tac_2str m'))
    1.50  ;
    1.51  
    1.52