# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1282299937 -7200
# Node ID 56f10b13005ea0ac68b73029071286eb923df382
# Parent  b65c6037eb6da8b27cfb563fc655657895a629c8
finished update ME/calchead.sml + pushed updates over all sml+test

not yet tackled in upcoming files:
# ProtoPure.thy          --> (theory "Pure")
# cterm_of (sign_of thy) --> (Thm.cterm thy)
# member op =            --> DONE, but TODO swap args
# string_of_cterm (cterm_of (sign_of " --> "(Syntax.string_of_term (thy2ctxt "
# Pattern.match
# there seem to be Problems with assoc_thy !?!

diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/IsacKnowledge/Test.ML
--- a/src/Tools/isac/IsacKnowledge/Test.ML	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/IsacKnowledge/Test.ML	Fri Aug 20 12:25:37 2010 +0200
@@ -538,13 +538,13 @@
     if atom t then true else bin_ops_only t;
 
 fun polynomial opl t bdVar = (* bdVar TODO *)
-    (bin_op t) subset opl andalso (bin_ops_only t);
+    subset op = (bin_op t, opl) andalso (bin_ops_only t);
 
 fun poly_equ opl bdVar t = is_equation t (* bdVar TODO *) 
     andalso polynomial opl (equ_lhs t) bdVar 
     andalso polynomial opl (equ_rhs t) bdVar
-    andalso ((varids bdVar) subset (varids (equ_lhs t))
-	     orelse(varids bdVar) subset (varids (equ_lhs t)));
+    andalso (subset op = (varids bdVar, varids (equ_lhs t)) orelse
+             subset op = (varids bdVar, varids (equ_lhs t)));
 
 (*fun max is =
     let fun max_ m [] = m 
@@ -563,7 +563,7 @@
 (*| deg _ _ v (_     (s,"?DUMMY"   ))          =   ..ML-error *) 
   | deg _ _ v((Const ("Bin.integ_of_bin",_)) $ _ )= 0 
   | deg addl mul v (h $ t1 $ t2) =
-    if(bin_op h)subset addl
+    if subset op = (bin_op h, addl)
     then max (deg addl mul v t1  ,deg addl mul v t2)
     else (*mul!*)(deg addl mul v t1)+(deg addl mul v t2)
 in if polynomial (addl @ [mul]) t bdVar
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/Isac_Mathengine.thy
--- a/src/Tools/isac/Isac_Mathengine.thy	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/Isac_Mathengine.thy	Fri Aug 20 12:25:37 2010 +0200
@@ -39,16 +39,16 @@
 
 
 ML {*
-thy2ctxt;
-thy2ctxt';
-SOME 111;
+111;
+member op = [1,2,3] 2;
 *}
 
 use "ME/calchead.sml"
 
 ML {*
-thy2ctxt;
-SOME 111;
+theory2theory';
+(assoc_thy "Script");
+(assoc_thy "Script.thy");
 *}
 
 (*
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/ME/appl.sml
--- a/src/Tools/isac/ME/appl.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/ME/appl.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -113,7 +113,7 @@
    ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
 > val p = [];
 > val (sss,ttt) = mk_set thy pt p consts pred;
-> (Syntax.string_of_term (thy2ctxt thy) sss,Sign.string_of_term(sign_of thy) ttt);
+> (Syntax.string_of_term (thy2ctxt thy) sss,Syntax.string_of_term(thy2ctxt thy) ttt);
 val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
 
  val consts = str2term "UniversalList";
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/ME/calchead.sml
--- a/src/Tools/isac/ME/calchead.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/ME/calchead.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -6,6 +6,8 @@
 
 use"ME/calchead.sml";
 use"calchead.sml";
+12345678901234567890123456789012345678901234567890123456789012345678901234567890
+        10        20        30        40        50        60        70        80
 *)
 
 (* TODO interne Funktionen aus sig entfernen *)
@@ -23,11 +25,11 @@
        (string * (Term.term * Term.term)) list -> cterm' -> additm
     type calcstate
     type calcstate'
-    val chk_vars : Thm.cterm SpecifyTools.ppc -> string * Term.term list
+    val chk_vars : term ppc -> string * Term.term list
     val chktyp :
-       theory -> int * Thm.cterm list * Thm.cterm list -> Thm.cterm
+       theory -> int * term list * term list -> term
     val chktyps :
-       theory -> Thm.cterm list * Thm.cterm list -> Thm.cterm list
+       theory -> term list * term list -> term list
     val complete_metitms :
    SpecifyTools.ori list ->
    SpecifyTools.itm list ->
@@ -193,10 +195,10 @@
        'b ->
        ptree ->
        (pos * pos_) * ((pos * pos_) * istate) * mout * tac * safe * ptree
-    val tag_form : theory -> Thm.cterm * Thm.cterm -> Thm.cterm
+    val tag_form : theory -> term * term -> term
     val test_types : theory -> Term.term * Term.term list -> string
     val typeless : Term.term -> Term.term
-    val unbound_ppc : Thm.cterm SpecifyTools.ppc -> Term.term list
+    val unbound_ppc : term SpecifyTools.ppc -> Term.term list
     val vals_of_oris : SpecifyTools.ori list -> Term.term list
     val variants_in : Term.term list -> int
     val vars_of_pbl_ : ('a * ('b * Term.term)) list -> Term.term list
@@ -279,31 +281,38 @@
 (*.to an input (d,ts) find the according ori and insert the ts.*)
 (*WN.11.03: + dont take first inter<>[]*)
 fun seek_oridts thy sel (d,ts) [] = 
-  ("'"^(Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy (d,ts)))^
- (*"' not found (typed)", e_ori_:ori, [])          ///11.11.03*)
+  ("'"^(Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts)))^
    "' not found (typed)", (0,[],sel,d,ts):ori, [])
   (* val (id,vat,sel',d',ts')::oris = ori;
      val (id,vat,sel',d',ts') = ori;
      *)
   | seek_oridts thy sel (d,ts) ((id,vat,sel',d',ts')::(oris:ori list)) =
-    if sel = sel' andalso d=d' andalso (ts inter ts') <> [] 
-      then if sel = sel' 
-	     then ("",(id,vat,sel,d, ts inter(*!overlap!*) ts'):ori, ts')
-	   else ((Syntax.string_of_term (thy2ctxt' thy) (comp_dts thy(d,ts)))^
-		 " not for "^sel, e_ori_, [])
+    if sel = sel' andalso d=d' andalso (inter op = ts ts') <> [] 
+    then if sel = sel' 
+	 then ("", 
+               (id,vat,sel,d, inter op = ts ts'):ori, 
+               ts')
+	 else ((Syntax.string_of_term (thy2ctxt thy) (comp_dts thy (d,ts))) 
+               ^ " not for " ^ sel, 
+               e_ori_, 
+               [])
     else seek_oridts thy sel (d,ts) oris;
 
 (*.to an input (_,ts) find the according ori and insert the ts.*)
 fun seek_orits thy sel ts [] = 
   ("'"^
-   (strs2str (map (Syntax.string_of_term (thy2ctxt' thy)) ts))^
+   (strs2str (map (Syntax.string_of_term (thy2ctxt thy)) ts))^
    "' not found (typed)", e_ori_, [])
   | seek_orits thy sel ts ((id,vat,sel',d,ts')::(oris:ori list)) =
-    if sel = sel' andalso (ts inter ts') <> [] 
+    if sel = sel' andalso (inter op = ts ts') <> [] 
       then if sel = sel' 
-	   then ("",(id,vat,sel,d,ts inter(*!overlap!*) ts'):ori, ts')
-	   else (((strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) ts)^
-		 " not for "^sel, e_ori_, [])
+	   then ("",
+                 (id,vat,sel,d, inter op = ts ts'):ori, 
+                 ts')
+	   else (((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
+                 ^ " not for "^sel, 
+                 e_ori_, 
+                 [])
     else seek_orits thy sel ts oris;
 (* false
 > val ((id,vat,sel',d,ts')::(ori':ori)) = ori;
@@ -345,7 +354,7 @@
       | coll eq  xs (y::ys) = 
       let val (n,ys') = cnt eq (y::ys) y 0;
       in if ys' = [] then xs @ n else coll eq  (xs @ n) ys' end;
-    val vts = (distinct (coll eq [] ts))\\[1];
+    val vts = subtract op = [1] (distinct (coll eq [] ts));
   in case vts of [] => 1 | [n] => n
       | _ => error "different variants in formalization" end;
 (*
@@ -397,35 +406,6 @@
 > has_list_type (term_of ct);
 val it = false : bool *)
 
-
-
-
-(*fdcrs = descriptions in formalization
-  unused 22.11.00
-fun is_already_input thy fdcrs ts t = 
-  let 
-    val tss = flat (map isalist2list ts);
-(*28.1.     val (dcr,t') = split_dsc_t fdcrs t; *)
-    val (dcr,[t']) = split_dts t;
-  in if (typeless t') mem (map typeless tss)
-            then ("term '"^(Syntax.string_of_term (thy2ctxt' thy) t')^
-		  "' already input")
-	  else "" end;
-
-> val pts = appc (map (term_of o the o (parse thy))) pbl;
-> val ts = #Relate pts;
-> val t = (term_of o the o (parse thy))"(A=#2*a*b - a^^^#2)";
-> is_already_input thy ts t;
-val it = "term 'A = #2 * a * b - a ^^^ #2' already input" : string
-> val t = (term_of o the o (parse thy))"a=#2*R*sin alpha";
-> is_already_input thy ts t;
-val it = "term 'a = #2 * R * sin alpha' already input" : string
-> val t = (term_of o the o (parse thy))"a=R*sin alpha";
-> is_already_input thy ts t;
-val it = "" : string
-*)
-
-
 fun is_parsed (Syn _) = false
   | is_parsed _ = true;
 fun parse_ok its = foldl and_ (true, map is_parsed its);
@@ -502,13 +482,15 @@
 (* val (_,_,fd,d,ts) = hd miss;
    *)
 fun getr_ct thy ((_,_,fd,d,ts):ori) =
-  (fd, (string_of_cterm o (comp_dts thy)) (d,[hd ts]):cterm');
+  (fd, ((Syntax.string_of_term (thy2ctxt thy)) o 
+        (comp_dts thy)) (d,[hd ts]):cterm');
 (* val t = comp_dts thy (d,[hd ts]);
    *)
 
 (* get a term from ori, notyet input in itm *)
 fun geti_ct thy ((_,_,_,d,ts):ori) ((_,_,_,fd,itm_):itm) =  
-  (fd, (string_of_cterm o (comp_dts thy)) (d,ts \\ (ts_in itm_)):cterm');
+  (fd, ((Syntax.string_of_term (thy2ctxt thy)) o (comp_dts thy)) 
+           (d, subtract op = (ts_in itm_) ts):cterm');
 (* test-maximum.sml fmy <> [], Init_Proof ...
    val (_,_,_,d,ts) = ori; val (_,_,_,fd,itm_) = hd icl;
    val d' $ ts' = (term_of o the o (parse thy)) "fixedValues [r=Arbfix]";
@@ -516,8 +498,8 @@
    atomty d';
    atomty (hd ts);
    atomty ts';
-   cterm_of (sign_of thy) (d $ (hd ts));
-   cterm_of (sign_of thy) (d' $ ts');
+   Thm.cterm_of thy (d $ (hd ts));
+   Thm.cterm_of thy (d' $ ts');
 
    comp_dts thy (d,ts);
    *)
@@ -530,6 +512,11 @@
 
 (* select an item in oris, notyet input in itms 
    (precondition: in itms are only Cor, Sup, Inc) *)
+local
+infix mem;
+fun x mem [] = false
+  | x mem (y :: ys) = x = y orelse x mem ys;
+in 
 fun nxt_add thy ([]:ori list) pbt itms = (*root (only) ori...fmz=[]*)
   let
     fun test_d d ((i,_,_,_,itm_):itm) = (d = (d_in itm_)) andalso i<>0; 
@@ -540,7 +527,7 @@
 (* val ((f,(d,_))::itms) = filter_out (is_elem itms) pbt;
    *)
     (f,(d,_))::itms => 
-      SOME (f:string, (string_of_cterm o comp_dts thy) (d,[]):cterm')
+      SOME (f:string, ((Syntax.string_of_term (thy2ctxt thy)) o comp_dts thy) (d,[]):cterm')
   | _ => NONE end
 
 (* val (thy,itms) = (assoc_thy (if dI=e_domID then dI' else dI),pbl);
@@ -554,7 +541,7 @@
 (* val itm = hd icl; val (_,_,_,d,ts) = v6;
    *)
     fun test_subset (itm:itm) ((_,_,_,d,ts):ori) = 
-	(d_in (#5 itm)) = d andalso (ts_in (#5 itm)) subset ts;
+	(d_in (#5 itm)) = d andalso subset op = (ts_in (#5 itm), ts);
     fun false_and_not_Sup((i,v,false,f,Sup _):itm) = false
       | false_and_not_Sup (i,v,false,f, _) = true
       | false_and_not_Sup  _ = false;
@@ -576,7 +563,8 @@
 	      *)
 	     NONE => raise error "nxt_add: EX itm. not(dat(itm)<=dat(ori))"
 	   | SOME ori => SOME (geti_ct thy ori (hd icl))
-  end;
+  end
+end;
 
 
 
@@ -699,10 +687,10 @@
 fun update_itm (cl,d,ts) ((id,vt,_,sl,Cor (_,_)):itm) = 
   (id,vt,cl,sl,Cor (d,ts)):itm
   | update_itm (cl,d,ts) (id,vt,_,sl,Syn (_)) =   
-  raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
+  raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Syn (s:cterm')")
   | update_itm (cl,d,ts) (id,vt,_,sl,Typ (_)) = 
-  raise error ("update_itm "^(string_of_cterm (comp_dts thy (d,ts)))^
+  raise error ("update_itm "^((Syntax.string_of_term (thy2ctxt thy)) (comp_dts thy (d,ts)))^
 	       " not not for Typ (s:cterm')")
   | update_itm (cl,d,ts) (id,vt,_,sl,Fal (_,_)) =
   (id,vt,cl,sl,Fal (d,ts))
@@ -718,7 +706,7 @@
 fun is_field_correct sel d dscpbt =
   case assoc (dscpbt, sel) of
     NONE => false
-  | SOME ds => d mem ds;
+  | SOME ds => member op = ds d;
 
 (*. update the itm_ already input, all..from ori .*)
 (* val (id,vt,fd,d,ts) = (i,v,f,d,ts\\ts');
@@ -729,7 +717,7 @@
     val pval = pbl_ids' thy d ts'
 	(*WN.9.5.03: FIXXXME [#0, epsilon]
 	  here would upd_penv be called for [#0, epsilon] etc. *)
-    val complete = if eq_set (ts', all) then true else false;
+    val complete = if eq_set op = (ts', all) then true else false;
   in case itm_ of
     (Cor _) => 
 	(if fd = "#undef" then (id,vt,complete,fd,Sup(d,ts')) 
@@ -774,42 +762,20 @@
       (case find_first (eq3 f d) itms of
 	   SOME (_,_,_,_,itm_) =>
 	   let 
-	       val ts' = (ts_in itm_) inter ts;
-	   in if ts subset ts' 
+	       val ts' = inter op = (ts_in itm_) ts;
+	   in if subset op = (ts, ts') 
 	      then (((strs2str' o 
-		      map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
+		      map (Syntax.string_of_term (thy2ctxt thy))) ts')^
 		    " already input", e_itm)                            (*2*)
-	      else ("", ori_2itm thy itm_ pid all (i,v,f,d,ts\\ts'))    (*3,4*)
+	      else ("", 
+                    ori_2itm thy itm_ pid all (i,v,f,d,
+                                               subtract op = ts' ts))   (*3,4*)
 	   end
 	 | NONE => ("", ori_2itm thy (Inc ((e_term,[]),(pid,[]))) 
 				 pid all (i,v,f,d,ts))                  (*1*)
 	)
     | NONE => ("", ori_2itm thy (Sup (d,ts)) 
 			      e_term all (i,v,f,d,ts));
-(*------------------------------------------------
-fun eq3 f d (_,_,_,f',itm_) = f = f' andalso d = (d_in itm_); 
-fun is_notyet_input thy itms pval all ((id,vt,fd,d,ts):ori) pbt =
-  case find_first (eq1 d) pbt of
-      SOME (_,(_,pid)) => (* val SOME (_,(_,pid)) = find_first (eq1 d) pbt;
-                              *)
-      (case seek_ppc id itms of
-	   SOME (id',_,_,_,itm_) =>
-	   let 
-	       val ts' = (ts_in itm_) inter ts;
-	   in if ts'= [] then ("", ori_2itm itm_ (pid, pval) all 
-					    (id,vt,fd,d,(ts_in itm_)@ts))
-	      else (((strs2str' o 
-		      map (Syntax.string_of_term (thy2ctxt' thy))) ts')^
-		    " already input", e_itm) end
-	 | NONE => 
-	   if all = ts 
-	   then ("", ori_2itm (Cor ((e_term,[]),(pid,[])))
-			      (pid, pval) all (id,vt,fd,d,ts))
-	   else ("", ori_2itm (Inc ((e_term,[]),(e_term,[]))) 
-			      (pid, pval) all (id,vt,fd,d,ts))
-	)
-    | NONE => ("", ori_2itm (Sup (e_term,[])) 
-			      (e_term, []) all (id,vt,fd,d,ts));----*)
 
 fun test_types thy (d,ts) =
   let 
@@ -817,9 +783,9 @@
     val opt = (try (comp_dts thy)) (d,ts);
     val msg = case opt of 
       SOME _ => "" 
-    | NONE => ((Sign.string_of_term  (sign_of thy) d)^" "^
-	     ((strs2str' o map (Sign.string_of_term(sign_of thy)))ts)
-	     ^" is illtyped");
+    | NONE => ((Syntax.string_of_term (thy2ctxt thy) d)^" "^
+	     ((strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) ts)
+	     ^ " is illtyped");
     val _ = show_types:= s
   in msg end;
 
@@ -846,16 +812,16 @@
     val (d,ts(*,pval*)) = split_dts thy t;
     val ids = map (fst o dest_Free) 
       ((distinct o (flat o (map vars))) ts);
-  in if (ids \\ oids) <> []
-     then (("identifiers "^(strs2str' (ids \\ oids))^
+  in if (subtract op = oids ids) <> []
+     then (("identifiers "^(strs2str' (subtract op = oids ids))^
 	    " not in example"), e_ori_, [])
      else 
 	 if d = e_term 
 	 then 
-	     if not ((map typeless ts) subset (map typeless ots))
+	     if not (subset op = (map typeless ts, map typeless ots))
 	     then (("terms '"^
-		    ((strs2str' o (map (Sign.string_of_term 
-					    (sign_of thy)))) ts)^
+		    ((strs2str' o (map (Syntax.string_of_term 
+					    (thy2ctxt thy)))) ts)^
 		    "' not in example (typeless)"), e_ori_, [])
 	     else (case seek_orits thy sel ts ori of
 		       ("", ori_ as (_,_,_,d,ts), all) =>
@@ -864,9 +830,9 @@
 			  | msg => (msg, e_ori_, []))
 		     | (msg,_,_) => (msg, e_ori_, []))
 	 else 
-	     if d mem (map #4 ori) 
+	     if member op = (map #4 ori) d
 	     then seek_oridts thy sel (d,ts) ori
-	     else ((Syntax.string_of_term (thy2ctxt' thy) d)^
+	     else ((Syntax.string_of_term (thy2ctxt thy) d)^
 		   (*" not in example", e_ori_, []) ///11.11.03*)
 		   " not in example", (0,[],sel,d,ts), [])
   end;
@@ -999,11 +965,11 @@
 (*.split type-wrapper from scr-arg and build part of an ori;
    an type-error is reported immediately, raises an exn, 
    subsequent handling of exn provides 2nd part of error message.*)
-fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
+(*fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =   WN100820 made cterm to term 
     (* val (thy, (str, (dsc, _)), (ty $ var)) =
 	   (thy,  p,               a);
        *)
-    (cterm_of (sign_of thy) (dsc $ var);(*type check*)
+    (Thm.cterm_of thy (dsc $ var);(*type check*)
      SOME ((([1], str, dsc, (*[var]*)
 	    split_dts' (dsc, var))): preori)(*:ori without leading #*))
     handle e  as TYPE _ => 
@@ -1017,6 +983,25 @@
 		      ^"*** checked by theory: "^(theory2str thy)^"\n"
 		      ^"*** "^dots 66);	     
 	     print_exn e; (*raises exn again*)
+	    NONE);*)
+fun mtc thy ((str, (dsc, _)):pat) (ty $ var) =
+    (* val (thy, (str, (dsc, _)), (ty $ var)) =
+	   (thy,  p,               a);
+       *)
+    (Thm.cterm_of thy (dsc $ var);(*type check*)
+     SOME ((([1], str, dsc, (*[var]*)
+	    split_dts' (dsc, var))): preori)(*:ori without leading #*))
+    handle e  as TYPE _ => 
+	   (writeln (dashs 70^"\n"
+		      ^"*** ERROR while creating the items for the model of the ->problem\n"
+		      ^"*** from the ->stac with ->typeconstructor in arglist:\n"
+		      ^"*** item (->description ->value): "^term2str dsc^" "^term2str var^"\n"
+		      ^"*** description: "^(term_detail2str dsc)
+		      ^"*** value: "^(term_detail2str var)
+		      ^"*** typeconstructor in script: "^(term_detail2str ty)
+		      ^"*** checked by theory: "^(theory2str thy)^"\n"
+		      ^"*** "^dots 66);	     
+	    (*WN100820 postponed: print_exn e; raises exn again*)
 	    NONE);
 (*> val pbt = (#ppc o get_pbt) ["univariate","equation"];
 > val Const ("Script.SubProblem",_) $
@@ -1139,7 +1124,8 @@
 fun overwrite_ppc thy itm ppc =
   let 
     fun repl ppc' (_,_,_,_,itm_) [] =
-      raise error ("overwrite_ppc: "^(itm__2str thy itm_)^" not found")
+      raise error ("overwrite_ppc: " ^ (itm_2str_ (thy2ctxt thy) itm_) ^ 
+                   " not found")
       | repl ppc' itm (p::ppc) =
 	if (#1 itm) = (#1 (p:itm)) then ppc' @ [itm] @ ppc
 	else repl (ppc' @ [p]) itm ppc
@@ -1186,9 +1172,9 @@
 
 
 (* test-printouts ---
-val _=writeln("### insert_ppc: (d,ts)="^(string_of_cterm(comp_dts thy(d,ts))));
+val _=writeln("### insert_ppc: (d,ts)="^((Syntax.string_of_term (thy2ctxt thy))(comp_dts thy(d,ts))));
  val _=writeln("### insert_ppc: pts= "^
-(strs2str' o map (Syntax.string_of_term (thy2ctxt' thy))) pts);
+(strs2str' o map (Syntax.string_of_term (thy2ctxt thy))) pts);
 
 
  val sel = "#Given"; val Add_Given' ct = m;
@@ -1384,6 +1370,7 @@
 		   meth=met, ...}) = get_obj I pt p;
     (*val pt = update_pbl pt p itms;
     val pt = update_pblID pt p pI;*)
+    val thy = assoc_thy dI
     val ((p,Pbl),_,_,pt)= 
 	generate1 thy (Specify_Problem' (pI, (ok, (itms, pre)))) Uistate pos pt
     val dI'' = assoc_thy (if dI=e_domID then dI' else dI);
@@ -1500,7 +1487,7 @@
 	   (*TODO.WN03 pass error-msgs to the frontend..
              FIXME ..and dont abuse a tactic for that purpose*)
 	   ([(Tac msg,
-	      Tac_ (ProtoPure.thy, msg,msg,msg),
+	      Tac_ (theory "Pure", msg,msg,msg),
 	      (e_pos', e_istate))], [], ptp) 
     end
 
@@ -1558,7 +1545,7 @@
 			      (#4:ori -> term)) oris;
     in filter_outs ors itms end;
 
-fun memI a b = b mem a;
+fun memI a b = member op = a b;
 (*filter oris which are in pbt, too*)
 fun filter_pbt oris pbt =
     let val dscs = map (fst o snd) pbt
@@ -1566,6 +1553,11 @@
 
 (*.combine itms from pbl + met and complete them wrt. pbt.*)
 (*FIXXXME.WN031205 complete_metitms doesnt handle incorrect itms !*)
+local
+infix mem;
+fun x mem [] = false
+  | x mem (y :: ys) = x = y orelse x mem ys;
+in 
 fun complete_metitms (oris:ori list) (pits:itm list) (mits:itm list) met = 
 (* val met = (#ppc o get_met) ["DiffApp","max_by_calculus"];
    *)
@@ -1575,11 +1567,17 @@
 	val ors = filter ((curry (op mem) vat) o (#2:ori -> int list)) oris;
         val os = filter_outs ors itms;
     (*WN.12.03?: does _NOT_ add itms from met ?!*)
-    in itms @ (map (ori2Coritm met) os) end;
+    in itms @ (map (ori2Coritm met) os) end
+end;
 
 
 
 (*.complete model and guard of a calc-head .*)
+local
+infix mem;
+fun x mem [] = false
+  | x mem (y :: ys) = x = y orelse x mem ys;
+in 
 fun complete_mod_ (oris, mpc, ppc, probl) =
     let	val pits = filter_out ((curry op= false) o (#3: itm -> bool)) probl
 	val vat = if probl = [] then 1 else max_vt probl
@@ -1589,7 +1587,8 @@
 
 	val pits = pits @ (map (ori2Coritm ppc) pors)
 	val mits = complete_metitms oris pits [] mpc
-    in (pits, mits) end;
+    in (pits, mits) end
+end;
 
 fun some_spec ((odI, opI, omI):spec) ((dI, pI, mI):spec) =
     (if dI = e_domID then odI else dI,
@@ -1606,6 +1605,7 @@
   let
     val (PblObj{origin=(oris,ospec,_),probl,spec,...}) = get_obj I pt p
     val (dI,pI,mI) = some_spec ospec spec
+    val thy = assoc_thy dI
     val mpc = (#ppc o get_met) mI (*just for reuse complete_mod_*)
     val {cas,ppc,...} = get_pbt pI
     val pbl = init_pbl ppc (*fill in descriptions*)
@@ -1634,6 +1634,7 @@
 	       val pbl = init_pbl ppc
 	       (*val pt = update_pbl pt p pbl ..done by Model_Problem*)
 	       val mI = if length met = 0 then e_metID else hd met
+               val thy = assoc_thy dI
 	       val (pos,c,_,pt) = 
 		   generate1 thy (Refine_Tacitly' (pI,pI',dI,mI,(*pbl*)[])) 
 			     Uistate pos pt
@@ -1710,9 +1711,16 @@
     raise error ("nxt_specif: not impl. for "^tac2str m');
 
 (*.get the values from oris; handle the term list w.r.t. penv.*)
+
+local
+infix mem;
+fun x mem [] = false
+  | x mem (y :: ys) = x = y orelse x mem ys;
+in 
 fun vals_of_oris oris =
     ((map (mkval' o (#5:ori -> term list))) o 
-     (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris;
+     (filter ((curry (op mem) 1) o (#2:ori -> int list)))) oris
+end;
 
 
 
@@ -1782,21 +1790,25 @@
       in f end;
 
 
-
-
-
-
-(* --------------------- ME --------------------- *)
-fun tag_form thy (formal, given) = cterm_of (sign_of thy) 
-	      (((head_of o term_of) given) $ (term_of formal));
+(*fun tag_form thy (formal, given) = Thm.cterm_of thy
+	      (((head_of o term_of) given) $ (term_of formal)); WN100819*)
+fun tag_form thy (formal, given) =
+    (let val gf = (head_of given) $ formal;
+         val _ = Thm.cterm_of thy gf
+     in gf end)
+    handle _ => raise error ("calchead.tag_form: " ^ 
+                             Syntax.string_of_term (thy2ctxt thy) given ^
+                             " .. " ^
+                             Syntax.string_of_term (thy2ctxt thy) formal ^
+                         " ..types do not match");
 (* val formal = (the o (parse thy)) "[R::real]";
 > val given = (the o (parse thy)) "fixed_values (cs::real list)";
 > tag_form thy (formal, given);
 val it = "fixed_values [R]" : cterm
 *)
 fun chktyp thy (n, fs, gs) = 
-  ((writeln o string_of_cterm o (nth n)) fs;
-   (writeln o string_of_cterm o (nth n)) gs;
+  ((writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) fs;
+   (writeln o (Syntax.string_of_term (thy2ctxt thy)) o (nth n)) gs;
    tag_form thy (nth n fs, nth n gs));
 
 fun chktyps thy (fs, gs) = map (tag_form thy) (fs ~~ gs);
@@ -1844,7 +1856,7 @@
 	  else ("ok",[]) end;*)
 fun chk_vars ctppc = 
   let val {Given=gi,Where=wh,Find=fi,With=wi,Relate=re} = 
-          appc flat (mappc (vars o term_of) ctppc)
+          appc flat (mappc vars ctppc)
       val chked = subtract op = gi wh
   in if chked <> [] then ("wh\\gi", chked)
      else let val chked = subtract op = (union op = gi fi) re
@@ -1857,7 +1869,7 @@
 (* check a new pbltype: variables (Free) unbound by given, find*) 
 fun unbound_ppc ctppc =
   let val {Given=gi,Find=fi,Relate=re,...} = 
-    appc flat (mappc (vars o term_of) ctppc)
+    appc flat (mappc vars ctppc)
   in distinct (*re\\(gi union fi)*) 
               (subtract op = (union op = gi fi) re) end;
 (*
@@ -1880,9 +1892,9 @@
   in ((fld f) o rev) xs end;
 (*
 > val (SOME ct) = parse thy "[a=b,c=d,e=f]";
-> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
+> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
 > val conj = foldr1 HOLogic.mk_conj (isalist2list (term_of ct));
-> cterm_of (sign_of thy) conj;
+> Thm.cterm_of thy conj;
 val it = "(a = b & c = d) & e = f" : cterm
 *)
 
@@ -1892,9 +1904,9 @@
   | foldl1 f (x::x'::xs) = f (x,foldl1 f (x'::xs));
 (*
 > val (SOME ct) = parse thy "[a=b,c=d,e=f,g=h]";
-> val ces = map (cterm_of (sign_of thy)) (isalist2list (term_of ct));
+> val ces = map (Thm.cterm_of thy) (isalist2list (term_of ct));
 > val conj = foldl1 HOLogic.mk_conj (isalist2list (term_of ct));
-> cterm_of (sign_of thy) conj;
+> Thm.cterm_of thy conj;
 val it = "a = b & c = d & e = f & g = h" : cterm
 *)
 
@@ -1920,8 +1932,7 @@
 *)
 
 (*fun eq1 d (_,(d',_)) = (d = d'); ---modspec.sml*)
-fun eq4 v (_,vts,_,_,_) = v mem vts;
-(*((curry (op mem)) (vat:int)) o (#2:ori -> int list);*)
+fun eq4 v (_,vts,_,_,_) = member op = vts v;
 fun eq5 (_,_,_,_,itm_) (_,_,_,d,_) = d_in itm_ = d;
 
  
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/ME/ctree.sml
--- a/src/Tools/isac/ME/ctree.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/ME/ctree.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -227,11 +227,6 @@
 
 fun subte2sube ss = map term2str ss;
 
-(*fun subst2str' thy' (s:subst) =
-  (strs2str o 
-   (map (pair2str o
-	 (apsnd (Sign.string_of_term (sign_of (assoc_thy thy')))) o 
-	 (apfst (Sign.string_of_term (sign_of (assoc_thy thy'))))))) s;*)
 fun subst2subs s = map (pair2str o 
 			(apfst (Syntax.string_of_term (thy2ctxt' "Isac"))) o
 			(apsnd (Syntax.string_of_term (thy2ctxt' "Isac")))) s;
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/ME/inform.sml
--- a/src/Tools/isac/ME/inform.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/ME/inform.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -227,7 +227,7 @@
 (* val itm as (i,v,b,f, Cor ((d,ts),_)) = hd probl;
    *)
     (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
-	 val s = Sign.string_of_term (sign_of dI) t;
+	 val s = Syntax.string_of_term (thy2ctxt dI) t;
      (*this    ^ should raise the exn on unability of re-parsing dts*)
      in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
   | parsitm dI (itm as (i,v,b,f, Syn str)) =
@@ -238,17 +238,17 @@
      in (i,v,b,f, Par str) end handle _ => (i,v,b,f, Syn str))
   | parsitm dI (itm as (i,v,_,f, Inc ((d,ts),_))) =
     (let val t = (term_of o comp_dts (Isac "delay")) (d,ts);
-	 val s = Sign.string_of_term (sign_of dI) t;
+	 val s = Syntax.string_of_term (thy2ctxt dI) t;
      (*this    ^ should raise the exn on unability of re-parsing dts*)
      in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
   | parsitm dI (itm as (i,v,_,f, Sup (d,ts))) =
     (let val t = (term_of o comp_dts (Isac"delay" )) (d,ts);
-	 val s = Sign.string_of_term (sign_of dI) t;
+	 val s = Syntax.string_of_term (thy2ctxt dI) t;
      (*this    ^ should raise the exn on unability of re-parsing dts*)
      in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
   | parsitm dI (itm as (i,v,_,f, Mis (d,t'))) =
     (let val t = d $ t';
-	 val s = Sign.string_of_term (sign_of dI) t;
+	 val s = Syntax.string_of_term (thy2ctxt dI) t;
      (*this    ^ should raise the exn on unability of re-parsing dts*)
      in itm end handle _ => ((i,v,false,f, Syn (term2str t)):itm))
   | parsitm dI (itm as (i,v,_,f, Par _)) = 
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/ME/script.sml
--- a/src/Tools/isac/ME/script.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/ME/script.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -105,13 +105,6 @@
 > val des = de_esc_underscore esc;
  val des = de_esc_underscore esc;*)
 
-
-(*WN.12.5.03 not used any more,
-  tacs are more stable than listepxr: subst_tacexpr
-fun is_listexpr t = 
-  (((ids_of o head_of) t) inter (!listexpr)) <> [];
-----*)
-
 (*go at a location in a script and fetch the contents*)
 fun go [] t = t
   | go (D::p) (Abs(s,ty,t0)) = go (p:loc_) t0
@@ -246,7 +239,7 @@
   | itr_arg _ (Const ("Script.SubProblem",_) $ _ $ _) = e_term
   | itr_arg thy t = raise error 
     ("itr_arg not impl. for "^
-     (Sign.string_of_term (sign_of (assoc_thy thy)) t));
+     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
 (* val t = (term_of o the o (parse thy))"Rewrite rroot_square_inv False e_";
 > itr_arg "Script.thy" t;
 val it = Free ("e_","RealDef.real") : term 
@@ -595,9 +588,9 @@
     (case stac of
 	 (t as Const ("Script.Rewrite",_) $ Free (thmID_,idT) $ b $ f_) =>
 	 ((*writeln("3### assod: stac = "^
-		    (Sign.string_of_term (sign_of (assoc_thy thy)) t));
+		    (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));
 	   writeln("3### assod: f(m)= "^
-		   (Sign.string_of_term (sign_of (assoc_thy thy)) f));*)
+		   (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) f));*)
 	  if thmID = thmID_ then 
 	      if f = f_ then ((*writeln"3### assod ..Ass";*)Ass (m,f')) 
 	      else ((*writeln"### assod ..AssWeak";
@@ -1563,7 +1556,7 @@
   | appy thy ptp E (*env*) l
   (Const ("Script.Repeat"(*2*),_) $ e) a v = 
     ((*writeln("3### appy Repeat: a= "^
-	     (Sign.string_of_term (sign_of (assoc_thy thy)) a));*)
+	     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) a));*)
      appy thy ptp E (*env*) (l@[R]) e a v)
 (* val (thy, ptp, E, l,      (t as Const ("Script.Try",_) $ e $ a), _, v)=
        (thy, ptp, E, (l@[R]), e2,                                   a, v);
@@ -1572,7 +1565,7 @@
   (t as Const ("Script.Try",_) $ e $ a) _ v =
   (case appy thy ptp E (l@[L,R]) e (SOME a) v of
      Napp E => ((*writeln("### appy Try "^
-			  (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+			  (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
 		 Skip (v, E))
    | ay => ay)
 (* val (thy, ptp, E, l,      (t as Const ("Script.Try",_) $ e), _, v)=
@@ -1584,7 +1577,7 @@
   (t as Const ("Script.Try",_) $ e) a v =
   (case appy thy ptp E (l@[R]) e a v of
      Napp E => ((*writeln("### appy Try "^
-			  (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+			  (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
 		 Skip (v, E))
    | ay => ay)
 
@@ -1688,7 +1681,7 @@
   | nxt_up thy ptp scr E l ay
     (t as Abs (_,_,_)) a v = 
     ((*writeln("### nxt_up Abs: "^
-	     (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+	     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
      nstep_up thy ptp scr E (*enr*) l ay a v)
 
   | nxt_up thy ptp scr E l ay
@@ -1696,7 +1689,7 @@
     ((*writeln("### nxt_up Let$e$Abs: is=");
      writeln(istate2str (ScrState (E,l,a,v,Sundef,false)));*)
      (*writeln("### nxt_up Let e Abs: "^
-	     (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+	     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
      nstep_up thy ptp scr (*upd_env*) E (*a,v)*) 
 	      (*eno,upd_env env (iar,res),iar,res,saf*) l ay a v)
 
@@ -1751,7 +1744,7 @@
   | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
   (t as Const ("Script.Try",_) $ e $ _) a v = 
     ((*writeln("### nxt_up Try "^
-	     (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+	     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
      nstep_up thy ptp scr E l Skip_ a v )
 (* val (thy, ptp, scr, E, l,   _,(t as Const ("Script.Try",_) $ e), a, v) =
        (thy, ptp, (Script sc), 
@@ -1760,7 +1753,7 @@
   | nxt_up thy ptp scr E l _ (*makes Napp to Skip*)
   (t as Const ("Script.Try"(*2*),_) $ e) a v = 
     ((*writeln("### nxt_up Try "^
-	     (Sign.string_of_term (sign_of (assoc_thy thy)) t));*)
+	     (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t));*)
      nstep_up thy ptp scr E l Skip_ a v)
 
 
@@ -1805,7 +1798,7 @@
 
   | nxt_up (thy,_) ptp scr E l ay t a v =
   raise error ("nxt_up not impl for "^
-	       (Sign.string_of_term (sign_of (assoc_thy thy)) t))
+	       (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) t))
 
 (* val (thy, ptp, (Script sc), E, l, ay,    a, v)=
        (thy, ptp, scr,         E, l, Skip_, a, v);
@@ -1815,13 +1808,13 @@
 and nstep_up thy ptp (Script sc) E l ay a v = 
   ((*writeln("### nstep_up from: "^(loc_2str l));
    writeln("### nstep_up from: "^
-	   (Sign.string_of_term (sign_of (assoc_thy thy)) (go l sc)));*)
+	   (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go l sc)));*)
    if 1 < length l
    then 
        let 
 	   val up = drop_last l; 
        in ((*writeln("### nstep_up to: "^
-	      (Sign.string_of_term (sign_of (assoc_thy thy)) (go up sc)));*)
+	      (Syntax.string_of_term (thy2ctxt (assoc_thy thy)) (go up sc)));*)
 	   nxt_up thy ptp (Script sc) E up ay (go up sc) a v ) end
    else (*interpreted to end*)
        if ay = Skip_ then Skip (v, E) else Napp E 
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/Scripts/term_G.sml
--- a/src/Tools/isac/Scripts/term_G.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/Scripts/term_G.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -9,13 +9,13 @@
 > cterm_of (sign_of thy) a_term;
 val it = "empty" : cterm        *)
 
-(*1003 fun match thy t pat =
+(*2003 fun match thy t pat =
     (snd (Pattern.match (Sign.tsig_of (sign_of thy)) (pat, t)))
     handle _ => [];
 fn : theory ->
      Term.term -> Term.term -> (Term.indexname * Term.term) list*)
 (*see src/Tools/eqsubst.ML fun clean_match*)
-(*1003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
+(*2003 fun matches thy tm pa = if match thy tm pa = [] then false else true;*)
 fun matches thy tm pa = 
     (Pattern.match thy (pa, tm) (Vartab.empty, Vartab.empty); true)
     handle _ => false
diff -r b65c6037eb6d -r 56f10b13005e src/Tools/isac/calcelems.sml
--- a/src/Tools/isac/calcelems.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/src/Tools/isac/calcelems.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -233,8 +233,6 @@
 type domID = string;   (* domID ^".thy" = theory' TODO.11.03replace by thyID*)
 type thyID = string;    (*WN.3.11.03 TODO: replace domID with thyID*)
 
-(*2002 fun string_of_thy thy = 
-((last_elem (Sign.stamp_names_of (sign_of thy)))^".thy"):theory';*)
 fun string_of_thy thy = Context.theory_name thy: theory';
 val theory2domID = string_of_thy;
 val theory2thyID = (get_thy o string_of_thy) : theory -> thyID;
@@ -596,16 +594,12 @@
 	    else ass ids
     in ass (!calclist') : calcID end;
 
-(*fun termopt2str (SOME t) = 
-    "SOME " ^ (Sign.string_of_term (sign_of(assoc_thy "Isac.thy")) t)
-  | termopt2str NONE = "NONE";*)
 fun termopt2str (SOME t) = 
     "SOME " ^ (Syntax.string_of_term (thy2ctxt' "Isac") t)
   | termopt2str NONE = "NONE";
 fun term2str t = Syntax.string_of_term (thy2ctxt' "Isac") t;
 fun terms2str ts= (strs2str o (map (Syntax.string_of_term 
 					(thy2ctxt' "Isac")))) ts;
-(*fun type2str typ = Sign.string_of_typ (sign_of (assoc_thy "Isac.thy")) typ;*)
 fun type2str typ = Syntax.string_of_typ (thy2ctxt' "Isac") typ;
 val string_of_typ = type2str;
 
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/IsacKnowledge/atools.sml
--- a/test/Tools/isac/IsacKnowledge/atools.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/IsacKnowledge/atools.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -24,7 +24,7 @@
 "----------- occurs_in -------------------------------------------";
 "----------- occurs_in -------------------------------------------";
 fun str2term str = (term_of o the o (parse thy )) str;
-fun term2s t = Sign.string_of_term (sign_of thy) t;
+fun term2s t = Syntax.string_of_term (thy2ctxt thy) t;
 val t = str2term "x";
 if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
 
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/IsacKnowledge/biegelinie.sml
--- a/test/Tools/isac/IsacKnowledge/biegelinie.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/IsacKnowledge/biegelinie.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -31,7 +31,7 @@
 "----------- the rules -------------------------------------------";
 "----------- the rules -------------------------------------------";
 fun str2term str = (term_of o the o (parse Biegelinie.thy)) str;
-fun term2s t = Sign.string_of_term (sign_of Biegelinie.thy) t;
+fun term2s t = Syntax.string_of_term (thy2ctxt' "Biegelinie") t;
 fun rewrit thm str = 
     fst (the (rewrite_ Biegelinie.thy tless_true e_rls true thm str));
 
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/IsacKnowledge/integrate.sml
--- a/test/Tools/isac/IsacKnowledge/integrate.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/IsacKnowledge/integrate.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -37,7 +37,7 @@
 "----------- parsing ---------------------------------------------";
 "----------- parsing ---------------------------------------------";
 fun str2term str = (term_of o the o (parse Integrate.thy)) str;
-fun term2s t = Sign.string_of_term (sign_of Integrate.thy) t;
+fun term2s t = Syntax.string_of_term (thy2ctxt' "Integrate") t;
     
 val t = str2term "Integral x D x";
 val t = str2term "Integral x^^^2 D x";
@@ -576,4 +576,4 @@
 (* WN070703 does not work like Diff due to error in next-pos
 if p = ([], Res) andalso term2str res = "5 * a" then ()
 else raise error "diff.sml behav.changed for Integrate (x^2 + x + 1, x)";
-*)
\ No newline at end of file
+*)
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/OLDTESTS/root-equ.sml
--- a/test/Tools/isac/OLDTESTS/root-equ.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -33,7 +33,7 @@
 > val t = (term_of o the o (parse thy)) "#2^^^#3";
 > val eval_fn = the (assoc (!eval_list, "pow"));
 > val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
-> Sign.string_of_term (sign_of thy) t';
+> Syntax.string_of_term (thy2ctxt thy) t';
 *)
 (******************************************************************)
 (*                  -------------------------------------         *)
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/OLDTESTS/script.sml
--- a/test/Tools/isac/OLDTESTS/script.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/OLDTESTS/script.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -92,19 +92,19 @@
 val SOME(l1,t1) = same_tacpbl sc ll (mI1,m1);
 loc_2str l1;
 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
-Sign.string_of_term (sign_of DiffApp.thy) t1;
+Syntax.string_of_term (thy2ctxt' "DiffApp") t1;
 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?6 ?4 *)
 
 val SOME(l2,t2) = same_tacpbl sc l1 (mI2,m2);
 loc_2str l2;
 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, L, R]"*)
-Sign.string_of_term (sign_of DiffApp.thy) t2;
+Syntax.string_of_term (thy2ctxt' "DiffApp") t2;
 (*"solve_univar (Reals, [univar, equation], no_met) B.1 B.3 "?7 ?3 *)
 
 val SOME(l3,t3) = same_tacpbl sc l2 (mI3,m3);
 loc_2str l3;
 (*"[R, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D, R, D]"*)
-Sign.string_of_term (sign_of DiffApp.thy) t3;
+Syntax.string_of_term (thy2ctxt' "DiffApp") t3;
 (*"Substitute [(v_1, (Rhs o hd) B.1), (v_2, (Rhs o hd) B.0)] B.8"*)
 
 
diff -r b65c6037eb6d -r 56f10b13005e test/Tools/isac/Scripts/calculate.sml
--- a/test/Tools/isac/Scripts/calculate.sml	Thu Aug 19 15:41:56 2010 +0200
+++ b/test/Tools/isac/Scripts/calculate.sml	Fri Aug 20 12:25:37 2010 +0200
@@ -36,19 +36,19 @@
 val t = (term_of o the o (parse thy)) "((1+2)*4/3)^^^2";
 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
+Syntax.string_of_term (thy2ctxt thy) t;
 (*val it = "(#3 * #4 // #3) ^^^ #2" : string*)
 val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times"))) t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
+Syntax.string_of_term (thy2ctxt thy) t;
 (*val it = "(#12 // #3) ^^^ #2" : string*)
 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"divide_")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
+Syntax.string_of_term (thy2ctxt thy) t;
 (*it = "#4 ^^^ #2" : string*)
 val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
 val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
-Sign.string_of_term (sign_of thy) t;
+Syntax.string_of_term (thy2ctxt thy) t;
 (*val it = "#16" : string*)
 if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
 else ();
@@ -388,22 +388,22 @@
  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"plus"))) t;
 "1 + 2 = 3";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ Syntax.string_of_term (thy2ctxt thy) t;
 "(3 * 4 / 3) ^^^ 2";
  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"times")))t;
 "3 * 4 = 12";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ Syntax.string_of_term (thy2ctxt thy) t;
 "(12 / 3) ^^^ 2";
  val SOME (thmID,thm) =get_calculation_ thy(the(assoc(calclist,"divide_")))t;
 "12 / 3 = 4";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ Syntax.string_of_term (thy2ctxt thy) t;
 "4 ^^^ 2";
  val SOME (thmID,thm) = get_calculation_ thy(the(assoc(calclist,"power_")))t;
 "4 ^^^ 2 = 16";
  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t;
- Sign.string_of_term (sign_of thy) t;
+ Syntax.string_of_term (thy2ctxt thy) t;
 "16";
  if it <> "16" then raise error "calculate.sml: new behaviour in calculate_"
  else ();