diff -r a0f2a165d552 -r 61f358925792 src/Tools/isac/Interpret/generate.sml
--- a/src/Tools/isac/Interpret/generate.sml	Wed May 04 14:07:51 2011 +0200
+++ b/src/Tools/isac/Interpret/generate.sml	Thu May 05 09:23:32 2011 +0200
@@ -295,12 +295,11 @@
 	pt) end
 
   | generate1 thy (Model_Problem' (_, itms, met)) _ (pos as (p,_)) pt =
-(* val (itms,pos as (p,_)) = (pbl, pos);
-   *)
-    let val pt = update_pbl pt p itms
-	val pt = update_met pt p met
-    in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef,
-			   (Upblmet,itms2itemppc thy [][]))), pt) end
+      let 
+        val pt = update_pbl pt p itms
+	      val pt = update_met pt p met
+     in (pos,[],Form'(PpcKF(0,EdUndef,0,Nundef, (Upblmet, itms2itemppc thy [] []))), pt)
+     end
 
   | generate1 thy (Refine_Tacitly' (pI,pIre,domID,metID,pbl)) 
 	      _ (pos as (p,_)) pt =