1.1 --- a/src/Tools/isac/Interpret/generate.sml	Wed May 04 14:07:51 2011 +0200
     1.2 +++ b/src/Tools/isac/Interpret/generate.sml	Thu May 05 09:23:32 2011 +0200
     1.3 @@ -295,12 +295,11 @@
     1.4  	pt) end
     1.5  
     1.6    | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
     1.7 -(* val (itms,pos as (p,_)) = (pbl, pos);
     1.8 -   *)
     1.9 -    let val pt = update_pbl pt p itms
    1.10 -	val pt = update_met pt p met
    1.11 -    in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,
    1.12 -			   (Upblmet,itms2itemppc thy [][]))), pt) end
    1.13 +      let 
    1.14 +        val pt = update_pbl pt p itms
    1.15 +	      val pt = update_met pt p met
    1.16 +     in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
    1.17 +     end
    1.18  
    1.19    | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) 
    1.20  	      _ (pos as (p,_)) pt =