1.1 --- a/src/Tools/isac/IsacKnowledge/Atools.ML	Thu Aug 19 15:36:02 2010 +0200
     1.2 +++ b/src/Tools/isac/IsacKnowledge/Atools.ML	Thu Aug 19 15:41:56 2010 +0200
     1.3 @@ -280,12 +280,12 @@
     1.4  	       (Const (op0,t0) $ t1 $ t2 )) thy = 
     1.5    if t1 = t2
     1.6      then SOME (mk_thmid thmid op0 
     1.7 -	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
     1.8 -	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"), 
     1.9 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
    1.10 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 
    1.11  	  Trueprop $ (mk_equality (t, true_as_term)))
    1.12    else SOME (mk_thmid thmid op0  
    1.13 -	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
    1.14 -	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"),  
    1.15 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
    1.16 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"),  
    1.17  	  Trueprop $ (mk_equality (t, false_as_term)))
    1.18    | eval_ident _ _ _ _ = NONE;
    1.19  (* TODO
    1.20 @@ -314,8 +314,8 @@
    1.21    if t1 = t2
    1.22      then ((*writeln"... eval_equal: t1 = t2  --> True";*)
    1.23  	  SOME (mk_thmid thmid op0 
    1.24 -	       ("("^(Sign.string_of_term (sign_of thy) t1)^")")
    1.25 -	       ("("^(Sign.string_of_term (sign_of thy) t2)^")"), 
    1.26 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t1)^")")
    1.27 +	       ("("^(Syntax.string_of_term (thy2ctxt thy) t2)^")"), 
    1.28  	  Trueprop $ (mk_equality (t, true_as_term)))
    1.29  	  )
    1.30    else (case (is_atom t1, is_atom t2) of

     2.1 --- a/src/Tools/isac/IsacKnowledge/Rational-WN.sml	Thu Aug 19 15:36:02 2010 +0200
     2.2 +++ b/src/Tools/isac/IsacKnowledge/Rational-WN.sml	Thu Aug 19 15:41:56 2010 +0200
     2.3 @@ -210,7 +210,7 @@
     2.4  		 val _ = if pairopt <> NONE then () 
     2.5  			 else raise error("rewrite_set_, rewrite_ \""^
     2.6  			 (string_of_thmI thm')^"\" \""^
     2.7 -			 (Sign.string_of_term (sign_of thy) ct)^"\" = NONE")
     2.8 +			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
     2.9  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
    2.10      val ruls = (#rules o rep_rls) ruless;
    2.11      val (ct',asm') = rew_once ruls [] ct Noap ruls;
    2.12 @@ -246,7 +246,7 @@
    2.13  		 val _ = if pairopt <> NONE then () 
    2.14  			 else raise error("rewrite_set_, rewrite_ \""^
    2.15  			 (string_of_thmI thm')^"\" \""^
    2.16 -			 (Sign.string_of_term (sign_of thy) ct)^"\" = NONE")
    2.17 +			 (Syntax.string_of_term (thy2ctxt thy) ct)^"\" = NONE")
    2.18  	       in rew_once ruls asm ((fst o the) pairopt) Appl(rul::thms) end);
    2.19      val ruls = (#rules o rep_rls) ruless;
    2.20      val (ct',asm') = rew_once ruls [] ct Noap ruls;

     3.1 --- a/src/Tools/isac/Isac_Mathengine.thy	Thu Aug 19 15:36:02 2010 +0200
     3.2 +++ b/src/Tools/isac/Isac_Mathengine.thy	Thu Aug 19 15:41:56 2010 +0200
     3.3 @@ -37,9 +37,17 @@
     3.4  use "ME/ptyps.sml"
     3.5  use "ME/generate.sml"
     3.6  
     3.7 +
     3.8 +ML {*
     3.9 +thy2ctxt;
    3.10 +thy2ctxt';
    3.11 +SOME 111;
    3.12 +*}
    3.13 +
    3.14  use "ME/calchead.sml"
    3.15  
    3.16  ML {*
    3.17 +thy2ctxt;
    3.18  SOME 111;
    3.19  *}
    3.20  

     4.1 --- a/src/Tools/isac/ME/appl.sml	Thu Aug 19 15:36:02 2010 +0200
     4.2 +++ b/src/Tools/isac/ME/appl.sml	Thu Aug 19 15:41:56 2010 +0200
     4.3 @@ -105,7 +105,7 @@
     4.4  
     4.5    | mk_set thy _ _ l _ = 
     4.6    raise error ("check_elementwise: no set "^
     4.7 -		 (Sign.string_of_term (sign_of thy) l));
     4.8 +		 (Syntax.string_of_term (thy2ctxt thy) l));
     4.9  (*> val consts = str2term "[x=#4]";
    4.10  > val pred = str2term "Assumptions";
    4.11  > val pt = union_asm pt p 
    4.12 @@ -113,7 +113,7 @@
    4.13     ("#0 <= x ^^^ #2 + #5 * x",[33]),("#0 <= #2 + x",[44])];
    4.14  > val p = [];
    4.15  > val (sss,ttt) = mk_set thy pt p consts pred;
    4.16 -> (Sign.string_of_term (sign_of thy) sss,Sign.string_of_term(sign_of thy) ttt);
    4.17 +> (Syntax.string_of_term (thy2ctxt thy) sss,Sign.string_of_term(sign_of thy) ttt);
    4.18  val it = ("x","((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) & ...
    4.19  
    4.20   val consts = str2term "UniversalList";

     5.1 --- a/src/Tools/isac/ME/script.sml	Thu Aug 19 15:36:02 2010 +0200
     5.2 +++ b/src/Tools/isac/ME/script.sml	Thu Aug 19 15:41:56 2010 +0200
     5.3 @@ -224,7 +224,7 @@
     5.4  fun init_form thy (Script sc) env =
     5.5    (case get_stac thy sc of
     5.6       NONE => NONE (*raise error ("init_form: no 1st stac in "^
     5.7 -			  (Sign.string_of_term (sign_of thy) sc))*)
     5.8 +			  (Syntax.string_of_term (thy2ctxt thy) sc))*)
     5.9     | SOME stac => SOME (subst_atomic env stac))
    5.10    | init_form _ _ _ = raise error "init_form: no match";
    5.11  
    5.12 @@ -301,7 +301,7 @@
    5.13  (*6.5.03 TODO: push penv into script -- and drop mk_arg here || drop penv
    5.14    9.5.03 penv postponed: penv = env for script at the moment, (*mk_arg*)*)
    5.15  fun mk_arg thy d [] = raise error ("mk_arg: no data for "^
    5.16 -			       (Sign.string_of_term (sign_of thy) d))
    5.17 +			       (Syntax.string_of_term (thy2ctxt thy) d))
    5.18    | mk_arg thy d [t] = 
    5.19      (case dsc_valT d of
    5.20  	 "una" => [t]
    5.21 @@ -310,7 +310,7 @@
    5.22  	      r as (Const ("op =",_) $ _ $ _) => r
    5.23  	    | _ => raise error 
    5.24  			     ("mk_arg: dsc-typ 'nam' applied to non-equality "^
    5.25 -			      (Sign.string_of_term (sign_of thy) t))]
    5.26 +			      (Syntax.string_of_term (thy2ctxt thy) t))]
    5.27         | s => raise error ("mk_arg: not impl. for "^s))
    5.28      
    5.29    | mk_arg thy d (t::ts) = (mk_arg thy d [t]) @ (mk_arg thy d ts);
    5.30 @@ -350,7 +350,7 @@
    5.31  > val mI = ("Script.thy","sqrt-equ-test");
    5.32  > val PblObj{meth={ppc=itms,...},...} = get_obj I pt [];
    5.33  > val ts = itms2args thy mI itms;
    5.34 -> map (Sign.string_of_term (sign_of thy)) ts;
    5.35 +> map (Syntax.string_of_term (thy2ctxt thy)) ts;
    5.36  ["sqrt (#9 + #4 * x) = sqrt x + sqrt (#5 + x)","x","#0"] : string list
    5.37  *)
    5.38  
    5.39 @@ -420,7 +420,7 @@
    5.40  (*12.1.01.*)
    5.41    | stac2tac_ pt thy (Const("Script.Check'_elementwise",_) $ _ $ 
    5.42  		    (set as Const ("Collect",_) $ Abs (_,_,pred))) = 
    5.43 -  (Check_elementwise (Sign.string_of_term (sign_of thy) pred), 
    5.44 +  (Check_elementwise (Syntax.string_of_term (thy2ctxt thy) pred), 
    5.45     (*set*)Empty_Tac_)
    5.46  
    5.47    | stac2tac_ pt thy (Const("Script.Or'_to'_List",_) $ _ ) = 
    5.48 @@ -475,7 +475,7 @@
    5.49  
    5.50    | stac2tac_ pt thy t = raise error 
    5.51    ("stac2tac_ TODO: no match for "^
    5.52 -   (Sign.string_of_term (sign_of thy) t));
    5.53 +   (Syntax.string_of_term (thy2ctxt thy) t));
    5.54  (*
    5.55  > val t = (term_of o the o (parse thy)) 
    5.56   "Rewrite_Set_Inst [(bdv,v_::real)] isolate_bdv False (x=a+#1)";
    5.57 @@ -541,7 +541,7 @@
    5.58    in (bdv, pred) end
    5.59    | rep_set thy _ _ set = 
    5.60      raise error ("check_elementwise: no set "^ (*from script*)
    5.61 -		 (Sign.string_of_term (sign_of thy) set));
    5.62 +		 (Syntax.string_of_term (thy2ctxt thy) set));
    5.63  (*> val set = (term_of o the o (parse thy)) "{(x::real). Assumptions}";
    5.64  > val p = [];
    5.65  > val pt = union_asm pt p [("#0 <= sqrt x + sqrt (#5 + x)",[11]),
    5.66 @@ -550,7 +550,7 @@
    5.67  			   ("#0 <= #2 + x",[44])];
    5.68  > val (bdv,pred) = rep_set thy pt p set;
    5.69  val bdv = Free ("x","RealDef.real") : term
    5.70 -> writeln (Sign.string_of_term (sign_of thy) pred);
    5.71 +> writeln (Syntax.string_of_term (thy2ctxt thy) pred);
    5.72  ((#0 <= sqrt x + sqrt (#5 + x) & #0 <= #9 + #4 * x) &
    5.73   #0 <= x ^^^ #2 + #5 * x) &
    5.74  #0 <= #2 + x
    5.75 @@ -834,16 +834,16 @@
    5.76    in (((make_rule (assoc_thy thy')) o HOLogic.mk_eq) (lhs,f'),(lhs,f')) end
    5.77  (*Fehlersuche 25.4.01
    5.78  (a)----- als String zusammensetzen:
    5.79 -ML> Sign.string_of_term (sign_of thy)f; 
    5.80 +ML> Syntax.string_of_term (thy2ctxt thy)f; 
    5.81  val it = "d_d x #4 + d_d x (x ^^^ #2 + #3 * x)" : string
    5.82 -ML> Sign.string_of_term (sign_of thy)f'; 
    5.83 +ML> Syntax.string_of_term (thy2ctxt thy)f'; 
    5.84  val it = "#0 + d_d x (x ^^^ #2 + #3 * x)" : string
    5.85  ML> subs;
    5.86  val it = [(Free ("bdv","RealDef.real"),Free ("x","RealDef.real"))] : subst
    5.87  > val tt = (term_of o the o (parse thy))
    5.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))";
    5.89  > atomty tt;
    5.90 -ML> writeln(Sign.string_of_term (sign_of thy)tt); 
    5.91 +ML> writeln(Syntax.string_of_term (thy2ctxt thy)tt); 
    5.92  (Rewrite_Inst [(bdv,x)] diff_const False d_d x #4 + d_d x (x ^^^ #2 + #3 * x)) =
    5.93   #0 + d_d x (x ^^^ #2 + #3 * x)
    5.94  

     6.1 --- a/src/Tools/isac/Scripts/Tools.sml	Thu Aug 19 15:36:02 2010 +0200
     6.2 +++ b/src/Tools/isac/Scripts/Tools.sml	Thu Aug 19 15:41:56 2010 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4    (t as (Const(op0,t0) $ arg)) thy = 
     6.5    let 
     6.6      val t' = ((list2isalist HOLogic.realT) o vars) t;
     6.7 -    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
     6.8 +    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
     6.9    in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    6.10    | eval_var _ _ _ _ = raise GO_ON;
    6.11  (* 
    6.12 @@ -21,14 +21,14 @@
    6.13  > val (SOME(thmId,t')) = eval_var thmid op0 t;
    6.14  val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
    6.15    : (string * term) option
    6.16 -> Sign.string_of_term (sign_of thy) t';
    6.17 +> Syntax.string_of_term (thy2ctxt thy) t';
    6.18  val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
    6.19  *)
    6.20  fun eval_Length (thmid:string) (op_:string) 
    6.21    (t as (Const(op0,t0) $ arg)) thy = 
    6.22    let 
    6.23      val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
    6.24 -    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
    6.25 +    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
    6.26    in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    6.27    | eval_Length _ _ _ _ = raise GO_ON;
    6.28  (*
    6.29 @@ -77,9 +77,9 @@
    6.30        let 
    6.31  	val t' = (nth (num_of_term t1) (isalist2list t2))
    6.32  	  handle _ => raise GO_ON; 
    6.33 -	val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^
    6.34 -	  "_"^(Sign.string_of_term (sign_of thy) t2)^
    6.35 -	  " = "^(Sign.string_of_term (sign_of thy) t');
    6.36 +	val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^
    6.37 +	  "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^
    6.38 +	  " = "^(Syntax.string_of_term (thy2ctxt thy) t');
    6.39        in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    6.40    else raise GO_ON
    6.41  )

     7.1 --- a/src/Tools/isac/Scripts/calculate.sml	Thu Aug 19 15:36:02 2010 +0200
     7.2 +++ b/src/Tools/isac/Scripts/calculate.sml	Thu Aug 19 15:41:56 2010 +0200
     7.3 @@ -139,79 +139,79 @@
     7.4  >  val t = (term_of o the o (parse thy)) "#3 + #4";
     7.5  >  val eval_fn = the (assoc (!eval_list, "op +"));
     7.6  >  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
     7.7 ->  Sign.string_of_term (sign_of thy) t';
     7.8 +>  Syntax.string_of_term (thy2ctxt thy) t';
     7.9  >  atomty t';
    7.10  > 
    7.11  >  val t = (term_of o the o (parse thy)) "(a + #3) + #4";
    7.12  >  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    7.13 ->  Sign.string_of_term (sign_of thy) t';
    7.14 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.15  > 
    7.16  >  val t = (term_of o the o (parse thy)) "#3 + (#4 + (a::real))";
    7.17  >  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    7.18 ->  Sign.string_of_term (sign_of thy) t';
    7.19 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.20  > 
    7.21  >  val t = (term_of o the o (parse thy)) "x = #5 * (#3 + (#4 + a))";
    7.22  >  atomty t;
    7.23  >  val (SOME (id,t')) = get_pair thy "op +" eval_fn t;
    7.24 ->  Sign.string_of_term (sign_of thy) t';
    7.25 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.26  >  val it = "#3 + (#4 + a) = #7 + a" : string
    7.27  >
    7.28  >
    7.29  >  val t = (term_of o the o (parse thy)) "#-4//#-2";
    7.30  >  val eval_fn = the (assoc (!eval_list, "cancel"));
    7.31  >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
    7.32 ->  Sign.string_of_term (sign_of thy) t';
    7.33 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.34  > 
    7.35  >  val t = (term_of o the o (parse thy)) "#2^^^#3";
    7.36  >  eval_binop "xxx" "pow" t thy;
    7.37  >  val eval_fn = (eval_binop "xxx")
    7.38  >		 : string -> term -> theory -> (string * term) option;
    7.39  >  val SOME (id,t') = get_pair thy "pow" eval_fn t;
    7.40 ->  Sign.string_of_term (sign_of thy) t';
    7.41 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.42  >  val eval_fn = the (assoc (!eval_list, "pow"));
    7.43  >  val (SOME (id,t')) = get_pair thy "pow" eval_fn t;
    7.44 ->  Sign.string_of_term (sign_of thy) t';
    7.45 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.46  > 
    7.47  >  val t = (term_of o the o (parse thy)) "x = #0 + #-1 * #-4";
    7.48  >  val eval_fn = the (assoc (!eval_list, "op *"));
    7.49  >  val (SOME (id,t')) = get_pair thy "op *" eval_fn t;
    7.50 ->  Sign.string_of_term (sign_of thy) t';
    7.51 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.52  > 
    7.53  >  val t = (term_of o the o (parse thy)) "#0 < #4";
    7.54  >  val eval_fn = the (assoc (!eval_list, "op <"));
    7.55  >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
    7.56 ->  Sign.string_of_term (sign_of thy) t';
    7.57 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.58  >  val t = (term_of o the o (parse thy)) "#0 < #-4";
    7.59  >  val (SOME (id,t')) = get_pair thy "op <" eval_fn t;
    7.60 ->  Sign.string_of_term (sign_of thy) t';
    7.61 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.62  > 
    7.63  >  val t = (term_of o the o (parse thy)) "#3 is_const";
    7.64  >  val eval_fn = the (assoc (!eval_list, "is'_const"));
    7.65  >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
    7.66 ->  Sign.string_of_term (sign_of thy) t';
    7.67 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.68  >  val t = (term_of o the o (parse thy)) "a is_const";
    7.69  >  val (SOME (id,t')) = get_pair thy "is'_const" eval_fn t;
    7.70 ->  Sign.string_of_term (sign_of thy) t';
    7.71 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.72  > 
    7.73  >  val t = (term_of o the o (parse thy)) "#6//(#8::real)";
    7.74  >  val eval_fn = the (assoc (!eval_list, "cancel"));
    7.75  >  val (SOME (id,t')) = get_pair thy "cancel" eval_fn t;
    7.76 ->  Sign.string_of_term (sign_of thy) t';
    7.77 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.78  > 
    7.79  >  val t = (term_of o the o (parse thy)) "sqrt #12";
    7.80  >  val eval_fn = the (assoc (!eval_list, "SqRoot.sqrt"));
    7.81  >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
    7.82 ->  Sign.string_of_term (sign_of thy) t';
    7.83 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.84  >  val it = "sqrt #12 = #2 * sqrt #3 " : string
    7.85  >
    7.86  >  val t = (term_of o the o (parse thy)) "sqrt #9";
    7.87  >  val (SOME (id,t')) = get_pair thy "SqRoot.sqrt" eval_fn t;
    7.88 ->  Sign.string_of_term (sign_of thy) t';
    7.89 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.90  >
    7.91  >  val t = (term_of o the o (parse thy)) "Nth #2 [#11,#22,#33]";
    7.92  >  val eval_fn = the (assoc (!eval_list, "Tools.Nth"));
    7.93  >  val (SOME (id,t')) = get_pair thy "Tools.Nth" eval_fn t;
    7.94 ->  Sign.string_of_term (sign_of thy) t';
    7.95 +>  Syntax.string_of_term (thy2ctxt thy) t';
    7.96  *)
    7.97  
    7.98  (* val ((op_, eval_fn),ct)=(cc,pre);

     8.1 --- a/src/Tools/isac/Scripts/rewrite.sml	Thu Aug 19 15:36:02 2010 +0200
     8.2 +++ b/src/Tools/isac/Scripts/rewrite.sml	Thu Aug 19 15:41:56 2010 +0200
     8.3 @@ -354,8 +354,8 @@
     8.4  
     8.5  
     8.6  (* for test-printouts:
     8.7 -val _ = writeln("in rew_sub  : "^( Sign.string_of_term (sign_of thy) t))
     8.8 -val _ = writeln("in eval_true: prems= "^(commas (map (Sign.string_of_term (sign_of thy)) prems')))
     8.9 +val _ = writeln("in rew_sub  : "^( Syntax.string_of_term (thy2ctxt thy) t))
    8.10 +val _ = writeln("in eval_true: prems= "^(commas (map (Syntax.string_of_term (thy2ctxt thy)) prems')))
    8.11  *)
    8.12  
    8.13