diff -r 2476f5f0f9ee -r 50bc995aa45b src/Tools/isac/Interpret/calchead.sml
--- a/src/Tools/isac/Interpret/calchead.sml	Wed Apr 06 18:01:02 2011 +0200
+++ b/src/Tools/isac/Interpret/calchead.sml	Thu Apr 07 16:31:05 2011 +0200
@@ -162,7 +162,7 @@
     val pt_model : ppobj -> pos_ -> ptform
     val reset_calchead : ptree * pos' -> ptree * pos'
     val seek_oridts :
-       theory ->
+       Proof.context ->
        string ->
        Term.term * Term.term list ->
        (int * SpecifyTools.vats * string * Term.term * Term.term list) list
@@ -205,11 +205,9 @@
 
 
 
-(*---------------------------------------------------------------------
 structure CalcHead (**): CALC_HEAD(**) =
 
 struct
----------------------------------------------------------------------*)
 
 (* datatypes *)
 
@@ -276,18 +274,6 @@
 
 (*.to an input (d,ts) find the according ori and insert the ts.*)
 (*WN.11.03: + dont take first inter<>[]*)
-(*fun seek_oridts ctxt sel (d,ts) [] =
-    ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
-                             (comp_dts (d,ts))) ^
-     "') not found in oris (typed)", (0, [], sel, d, ts) : ori,
-     [])
-  | seek_oridts ctxt sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
-    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> []
-	 then ("", 
-               (id,vat,sel,d, inter op = ts ts'):ori, 
-               ts')
-    else seek_oridts ctxt sel (d,ts) oris;*)
-
 fun seek_oridts ctxt sel (d,ts) [] =
     ("seek_oridts: input ('" ^ (Print_Mode.setmp [] (Syntax.string_of_term ctxt)
                              (comp_dts (d,ts))) ^
@@ -791,10 +777,10 @@
 fun appl_add ctxt sel [] ppc pbt t =
       let
         val i = 1 + (if ppc = [] then 0 else map #1 ppc |> maxl);
-      in case parseNEW ctxt t of
+      in case parse (ProofContext.theory_of ctxt) t of
           NONE => Add (i, [], false, sel, Syn t)
         | SOME t' =>
-          let val (d, ts) = split_dts t';
+          let val (d, ts) = split_dts (term_of t');
           in if d = e_term then
             Add (i, [], false, sel, Mis (dsc_unknown, hd ts)) else
             (case find_first (eq1 d) pbt of
@@ -820,9 +806,9 @@
             end
       end
   | appl_add ctxt sel oris ppc pbt str =
-      case parseNEW ctxt str of
+      case parse (ProofContext.theory_of ctxt) str of
           NONE => Err ("appl_add: syntax error in '" ^ str ^ "'")
-        | SOME t => case is_known ctxt sel oris t of
+        | SOME t => case is_known ctxt sel oris (term_of t) of
             ("", ori', all) => (case is_notyet_input ctxt ppc all ori' pbt of
               ("", itm) => Add itm
               | (msg, _) => Err msg)
@@ -1066,7 +1052,7 @@
     end
 (* val (p,_) = p;
    *)
-| specify_additem sel (ct,_) (p,p_(*Frm, Pbl*)) c pt = 
+| specify_additem sel (ct,_) (p,_(*Frm, Pbl*)) c pt = 
     let
       val (PblObj{meth=met,origin=(oris,(dI',pI',mI'),_),
 		  probl=pbl,spec=(dI,pI,mI),...}) = get_obj I pt p;
@@ -1127,10 +1113,9 @@
 fun specify (Init_Proof' (fmz,(dI',pI',mI'))) (_:pos') (_:cid) (_:ptree)= 
   let          (* either """"""""""""""" all empty or complete *)
     val thy = assoc_thy dI';
-    val (istate_, ctxt) = (#ppc o get_pbt) pI' |> prep_ori fmz thy;
     val oris = if dI' = e_domID orelse pI' = e_pblID then ([]:ori list)
-	       else istate_;
-    val (pt,c) = cappend_problem e_ptree [] (e_istate, ctxt) (fmz,(dI',pI',mI'))
+	       else pI' |> #ppc o get_pbt |> prep_ori fmz thy |> #1;
+    val (pt,c) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz,(dI',pI',mI'))
 				 (oris,(dI',pI',mI'),e_term);
     val {ppc,prls,where_,...} = get_pbt pI'
     (*val pbl = init_pbl ppc;  WN.9.03: done in Model/Refine_Problem
@@ -1579,7 +1564,7 @@
 	let val {ppc,...} = get_met mI
 	    val dI = if dI = "" then "Isac" else dI
 	    val thy = assoc_thy dI;
-	    val (pt,_) = cappend_problem e_ptree [] (Uistate, e_ctxt) ([], (dI,pI,mI))
+	    val (pt,_) = cappend_problem e_ptree [] (e_istate, e_ctxt) ([], (dI,pI,mI))
 					 ([], (dI,pI,mI), e_term(*FIXME met*));
 	    val pt = update_spec pt [] (dI,pI,mI);
 	    val mits = init_pbl' ppc;
@@ -1601,12 +1586,11 @@
 	    else (pI, get_pbt pI |> #ppc |> prep_ori fmz thy |> #1, mI)
 	val {cas, ppc, thy=thy',...} = get_pbt pI (*take dI from _refined_ pbl*)
 	val dI = theory2theory' (maxthy thy thy');
-	val ctxt = prep_ori fmz thy ppc |> #2;
 	val hdl = case cas of
 		      NONE => pblterm dI pI
 		    | SOME t => subst_atomic ((vars_of_pbl_' ppc) 
 						  ~~~ vals_of_oris pors) t;
-        val (pt, _) = cappend_problem e_ptree [] (Uistate, ctxt) (fmz, (dI, pI, mI))
+        val (pt, _) = cappend_problem e_ptree [] (e_istate, e_ctxt) (fmz, (dI, pI, mI))
 				      (pors, (dI, pI, mI), hdl)
     in ((pt, ([], Pbl)), 
         fst3 (nxt_specif Model_Problem (pt, ([], Pbl)))) : calcstate
@@ -2081,9 +2065,6 @@
 	val pt = update_spec pt p e_spec
     in (pt, (p,Pbl):pos') end;
 
-(*---------------------------------------------------------------------
 end
 
 open CalcHead;
----------------------------------------------------------------------*)
-