diff -r 1ada058e92bc -r 2301fe2b9f9c src/Tools/isac/Interpret/calchead.sml
--- a/src/Tools/isac/Interpret/calchead.sml	Sun May 15 11:32:41 2011 +0200
+++ b/src/Tools/isac/Interpret/calchead.sml	Sun May 15 12:36:29 2011 +0200
@@ -997,90 +997,82 @@
 	     | pos => error ("header called with "^ pos_2str pos);
 
 
-fun specify_additem sel (ct,_) (p,Met) c pt = 
-    let
-      val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
-		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
-      val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
-    (*val ppt = if pI = e_pblID then get_pbt pI' else get_pbt pI;*)
-      val cpI = if pI = e_pblID then pI' else pI;
-      val cmI = if mI = e_metID then mI' else mI;
-      val {ppc,pre,prls,...} = get_met cmI;
-    in case appl_add ctxt sel oris met ppc ct of
-      Add itm (*..union old input *) =>
-	let (* val Add itm = appl_add thy sel oris met (#ppc (get_met cmI)) ct;
-               *)
-	  val met' = insert_ppc thy itm met;
-	  (*val pt' = update_met pt p met';*)
-	  val ((p,Met),_,_,pt') = 
-	      generate1 thy (case sel of
-				 "#Given" => Add_Given' (ct, met')
-			       | "#Find"  => Add_Find'  (ct, met')
-			       | "#Relate"=> Add_Relation'(ct, met')) 
-			(Uistate, e_ctxt) (p,Met) pt
-	  val pre' = check_preconds thy prls pre met'
-	  val pb = foldl and_ (true, map fst pre')
-	  (*val _=tracing("@@@ specify_additem: Met Add before nxt_spec")*)
-	  val (p_,nxt) =
-	    nxt_spec Met pb oris (dI',pI',mI') (pbl,met') 
-	    ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
-	in ((p,p_), ((p,p_),Uistate),
-	    Form' (PpcKF (0,EdUndef,(length p),Nundef,
-			  (Method cmI, itms2itemppc thy met' pre'))),
-	    nxt,Safe,pt') end
-    | Err msg =>
-	  let val pre' = check_preconds thy prls pre met
-	      val pb = foldl and_ (true, map fst pre')
-	    (*val _=tracing("@@@ specify_additem: Met Err before nxt_spec")*)
-	      val (p_,nxt) =
-	    nxt_spec Met pb oris (dI',pI',mI') (pbl,met) 
-	    ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
-	  in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
-    end
-(* val (p,_) = p;
-   *)
-| specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
-    let
-      val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
-		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
-      val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
-      val cpI = if pI = e_pblID then pI' else pI;
-      val cmI = if mI = e_metID then mI' else mI;
-      val {ppc,where_,prls,...} = get_pbt cpI;
-    in case appl_add ctxt sel oris pbl ppc ct of
-      Add itm (*..union old input *) =>
-      (* val Add itm = appl_add thy sel oris pbl ppc ct;
-         *)
-	let
-	    (*val _= tracing("###specify_additem: itm= "^(itm2str_ itm));*)
-	  val pbl' = insert_ppc thy itm pbl
-	  val ((p,Pbl),_,_,pt') = 
-	      generate1 thy (case sel of
-				 "#Given" => Add_Given' (ct, pbl')
-			       | "#Find"  => Add_Find'  (ct, pbl')
-			       | "#Relate"=> Add_Relation'(ct, pbl')) 
-			(Uistate, e_ctxt) (p,Pbl) pt
-	  val pre = check_preconds thy prls where_ pbl'
-	  val pb = foldl and_ (true, map fst pre)
-	(*val _=tracing("@@@ specify_additem: Pbl Add before nxt_spec")*)
-	  val (p_,nxt) =
-	    nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) 
-		     (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
-	  val ppc = if p_= Pbl then pbl' else met;
-	in ((p,p_), ((p,p_),Uistate),
-	    Form' (PpcKF (0,EdUndef,(length p),Nundef,
-			  (header p_ pI cmI,
-			   itms2itemppc thy ppc pre))), nxt,Safe,pt') end
+fun specify_additem sel (ct,_) (p, Met) c pt = 
+      let
+        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
+  		    probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
+        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
+        val cpI = if pI = e_pblID then pI' else pI;
+        val cmI = if mI = e_metID then mI' else mI;
+        val {ppc,pre,prls,...} = get_met cmI;
+      in 
+        case appl_add ctxt sel oris met ppc ct of
+          Add itm (*..union old input *) =>
+  	        let
+              val met' = insert_ppc thy itm met;
+  	          val ((p, Met), _, _, pt') = 
+  	            generate1 thy (case sel of
+  				                       "#Given" => Add_Given'   (ct, met')
+  			                       | "#Find"  => Add_Find'    (ct, met')
+  			                       | "#Relate"=> Add_Relation'(ct, met')) 
+  			        (Uistate, e_ctxt) (p, Met) pt
+  	          val pre' = check_preconds thy prls pre met'
+  	          val pb = foldl and_ (true, map fst pre')
+  	          val (p_, nxt) =
+  	            nxt_spec Met pb oris (dI',pI',mI') (pbl,met') 
+  	              ((#ppc o get_pbt) cpI,ppc) (dI,pI,mI);
+  	        in ((p, p_), ((p, p_), Uistate),
+  	          Form' (PpcKF (0,EdUndef,(length p),Nundef,
+  			        (Method cmI, itms2itemppc thy met' pre'))), nxt,Safe,pt')
+            end
+        | Err msg =>
+  	        let
+              val pre' = check_preconds thy prls pre met
+  	          val pb = foldl and_ (true, map fst pre')
+  	          val (p_, nxt) =
+  	            nxt_spec Met pb oris (dI',pI',mI') (pbl,met) 
+  	              ((#ppc o get_pbt) cpI,(#ppc o get_met) cmI) (dI,pI,mI);
+  	        in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
+      end
 
-    | Err msg =>
-	  let val pre = check_preconds thy prls where_ pbl
-	      val pb = foldl and_ (true, map fst pre)
-	    (*val _=tracing("@@@ specify_additem: Pbl Err before nxt_spec")*)
-	      val (p_,nxt) =
-	    nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 
-	    (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
-	  in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
-    end;
+  | specify_additem sel (ct,_) (pos as (p,_(*Frm, Pbl*))) c pt = 
+      let
+        val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
+		      probl=pbl,spec=(dI,pI,mI), ctxt, ...}) = get_obj I pt p;
+        val thy = if dI = e_domID then assoc_thy dI' else assoc_thy dI;
+        val cpI = if pI = e_pblID then pI' else pI;
+        val cmI = if mI = e_metID then mI' else mI;
+        val {ppc,where_,prls,...} = get_pbt cpI;
+      in
+        case appl_add ctxt sel oris pbl ppc ct of
+          Add itm (*..union old input *) =>
+	          let
+	            val pbl' = insert_ppc thy itm pbl
+	            val ((p, Pbl), _, _, pt') = 
+	              generate1 thy (case sel of
+				                         "#Given" => Add_Given'   (ct, pbl')
+			                         | "#Find"  => Add_Find'    (ct, pbl')
+			                         | "#Relate"=> Add_Relation'(ct, pbl')) 
+			           (Uistate, e_ctxt) (p,Pbl) pt
+	            val pre = check_preconds thy prls where_ pbl'
+	            val pb = foldl and_ (true, map fst pre)
+	            val (p_, nxt) =
+	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl',met) 
+		              (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
+	            val ppc = if p_= Pbl then pbl' else met;
+	          in ((p,p_), ((p,p_),Uistate),
+	            Form' (PpcKF (0,EdUndef,(length p),Nundef,
+			          (header p_ pI cmI, itms2itemppc thy ppc pre))), nxt,Safe,pt')
+            end
+        | Err msg =>
+	          let
+              val pre = check_preconds thy prls where_ pbl
+	            val pb = foldl and_ (true, map fst pre)
+	            val (p_, nxt) =
+	              nxt_spec Pbl pb oris (dI',pI',mI') (pbl,met) 
+	                (ppc,(#ppc o get_met) cmI) (dI,pI,mI);
+	          in ((p,p_), ((p,p_),Uistate), Error' (Error_ msg), nxt, Safe,pt) end
+      end;
 
 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 
   let          (* either """"""""""""""" all empty or complete *)