1.1 --- a/src/Tools/isac/Interpret/solve.sml	Fri May 20 14:08:14 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/solve.sml	Fri May 20 14:49:07 2011 +0200
     1.3 @@ -181,8 +181,8 @@
     1.4        in ("ok", ([(Empty_Tac, Empty_Tac_, (po, (Uistate, e_ctxt)))], [], (pt,p')))
     1.5        end
     1.6  
     1.7 -  | solve ("Check_Postcond",Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
     1.8 -      let (*val _=tracing"###solve Check_Postcond";*)
     1.9 +  | solve ("Check_Postcond", Check_Postcond' (pI,_)) (pt,(pos as (p,p_))) =
    1.10 +      let
    1.11          val pp = par_pblobj pt p
    1.12          val asm = 
    1.13            (case get_obj g_tac pt p of
    1.14 @@ -201,7 +201,7 @@
    1.15          then
    1.16  	        let 
    1.17              val is = ScrState (E,l,a,scval,scsaf,b)
    1.18 -	          val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
    1.19 +	          val tac_ = Check_Postcond' (pI, (scval, asm))
    1.20  	          val (pos,ps,f,pt) = generate1 thy tac_ (is, ctxt) (pp,Res) pt;
    1.21  	        in ("ok", ([(Check_Postcond pI, tac_, ((pp,Res),(is, ctxt)))], ps,(pt,pos))) end
    1.22          else
    1.23 @@ -214,9 +214,9 @@
    1.24              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm); 
    1.25  	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
    1.26              val ((p,p_),ps,f,pt) = 
    1.27 -	            generate1 thy (Check_Postcond' (pI, (scval, map term2str asm)))
    1.28 +	            generate1 thy (Check_Postcond' (pI, (scval, asm)))
    1.29  		            (ScrState (E,l,a,scval,scsaf,b), ctxt'') (pp,Res) pt;
    1.30 -       in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, map term2str asm)),
    1.31 +       in ("ok", ([(Check_Postcond pI, Check_Postcond'(pI,(scval, asm)),
    1.32  	         ((pp,Res), (ScrState (E,l,a,scval,scsaf,b), ctxt'')))],ps,(pt,(p,p_))))
    1.33  	     end
    1.34       end
    1.35 @@ -320,7 +320,7 @@
    1.36          then 
    1.37  	        let
    1.38              val is = ScrState (E,l,a,scval,scsaf,b)
    1.39 -	          val tac_ = Check_Postcond'(pI,(scval, map term2str asm))
    1.40 +	          val tac_ = Check_Postcond'(pI,(scval, asm))
    1.41  	          val ((p,p_),ps,f,pt) = 
    1.42  		          generate1 thy tac_ (is, ctxt) (pp,Res) pt;
    1.43  	        in ([(Check_Postcond pI, tac_, ((pp,Res), (is, ctxt)))],ps,(pt, (p,p_))) end
    1.44 @@ -333,7 +333,7 @@
    1.45  	          val {scr,...} = get_met metID;
    1.46              val (ScrState (E,l,a,_,_,b), ctxt') = get_loc pt (pp(*!/p/*),Frm)
    1.47  	          val ctxt'' = transfer_from_subproblem ctxt ctxt'
    1.48 -            val tac_ = Check_Postcond' (pI, (scval, map term2str asm))
    1.49 +            val tac_ = Check_Postcond' (pI, (scval, asm))
    1.50  	          val is = ScrState (E,l,a,scval,scsaf,b)
    1.51              val ((p,p_),ps,f,pt) = generate1 thy tac_ (is, ctxt'') (pp, Res) pt;
    1.52            in ([(Check_Postcond pI, tac_, ((pp, Res), (is, ctxt'')))], ps, (pt, (p,p_))) end