1.1 --- a/src/Tools/isac/ME/script.sml	Thu Aug 19 15:36:02 2010 +0200
     1.2 +++ b/src/Tools/isac/ME/script.sml	Thu Aug 19 15:41:56 2010 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4  fun init_form thy (Script sc) env =
     1.5    (case get_stac thy sc of
     1.6       NONE => NONE (*raise error ("init_form: no 1st stac in "^
     1.7 -			  (Sign.string_of_term (sign_of thy) sc))*)
     1.8 +			  (Syntax.string_of_term (thy2ctxt thy) sc))*)
     1.9     | SOME stac => SOME (subst_atomic env stac))
    1.10    | init_form _ _ _ = raise error "init_form: no match";
    1.11  
    1.12 @@ -301,7 +301,7 @@
    1.13  (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
    1.14    9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
    1.15  fun mk_arg thy d [] = raise error ("mk_arg: no data for "^
    1.16 -			       (Sign.string_of_term (sign_of thy) d))
    1.17 +			       (Syntax.string_of_term (thy2ctxt thy) d))
    1.18    | mk_arg thy d [t] = 
    1.19      (case dsc_valT d of
    1.20  	 "una" => [t]
    1.21 @@ -310,7 +310,7 @@
    1.22  	      r as (Const ("op =",_) $ _ $ _) => r
    1.23  	    | _ => raise error 
    1.24  			     ("mk_arg: dsc-typ 'nam' applied to non-equality "^
    1.25 -			      (Sign.string_of_term (sign_of thy) t))]
    1.26 +			      (Syntax.string_of_term (thy2ctxt thy) t))]
    1.27         | s => raise error ("mk_arg: not impl. for "^s))
    1.28      
    1.29    | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
    1.30 @@ -350,7 +350,7 @@
    1.31  > val mI = ("Script.thy","sqrt-equ-test");
    1.32  > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
    1.33  > val ts = itms2args thy mI itms;
    1.34 -> map (Sign.string_of_term (sign_of thy)) ts;
    1.35 +> map (Syntax.string_of_term (thy2ctxt thy)) ts;
    1.36  ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
    1.37  *)
    1.38  
    1.39 @@ -420,7 +420,7 @@
    1.40  (*12.1.01.*)
    1.41    | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ 
    1.42  		    (set as Const ("Collect",_) $ Abs (_,_,pred))) = 
    1.43 -  (Check_elementwise (Sign.string_of_term (sign_of thy) pred), 
    1.44 +  (Check_elementwise (Syntax.string_of_term (thy2ctxt thy) pred), 
    1.45     (*set*)Empty_Tac_)
    1.46  
    1.47    | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = 
    1.48 @@ -475,7 +475,7 @@
    1.49  
    1.50    | stac2tac_ pt thy t = raise error 
    1.51    ("stac2tac_ TODO: no match for "^
    1.52 -   (Sign.string_of_term (sign_of thy) t));
    1.53 +   (Syntax.string_of_term (thy2ctxt thy) t));
    1.54  (*
    1.55  > val t = (term_of o the o (parse thy)) 
    1.56   "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";
    1.57 @@ -541,7 +541,7 @@
    1.58    in (bdv, pred) end
    1.59    | rep_set thy _ _ set = 
    1.60      raise error ("check_elementwise: no set "^ (*from script*)
    1.61 -		 (Sign.string_of_term (sign_of thy) set));
    1.62 +		 (Syntax.string_of_term (thy2ctxt thy) set));
    1.63  (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}";
    1.64  > val p = [];
    1.65  > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]),
    1.66 @@ -550,7 +550,7 @@
    1.67  			   ("#0 <= #2 + x",[44])];
    1.68  > val (bdv,pred) = rep_set thy pt p set;
    1.69  val bdv = Free ("x","RealDef.real") : term
    1.70 -> writeln (Sign.string_of_term (sign_of thy) pred);
    1.71 +> writeln (Syntax.string_of_term (thy2ctxt thy) pred);
    1.72  ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) &
    1.73   #0 <= x ^^^ #2 + #5 * x) &
    1.74  #0 <= #2 + x
    1.75 @@ -834,16 +834,16 @@
    1.76    in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
    1.77  (*Fehlersuche 25.4.01
    1.78  (a)----- als String zusammensetzen:
    1.79 -ML> Sign.string_of_term (sign_of thy)f; 
    1.80 +ML> Syntax.string_of_term (thy2ctxt thy)f; 
    1.81  val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
    1.82 -ML> Sign.string_of_term (sign_of thy)f'; 
    1.83 +ML> Syntax.string_of_term (thy2ctxt thy)f'; 
    1.84  val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
    1.85  ML> subs;
    1.86  val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
    1.87  > val tt = (term_of o the o (parse thy))
    1.88    "(Rewrite_Inst[(bdv,x)]diff_const False(d_d x #4 + d_d x (x ^^^ #2 + #3 * x)))=(#0 + d_d x (x ^^^ #2 + #3 * x))";
    1.89  > atomty tt;
    1.90 -ML> writeln(Sign.string_of_term (sign_of thy)tt); 
    1.91 +ML> writeln(Syntax.string_of_term (thy2ctxt thy)tt); 
    1.92  (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
    1.93   #0 + d_d x (x ^^^ #2 + #3 * x)
    1.94