1.1 --- a/src/Tools/isac/Scripts/Tools.sml	Thu Aug 19 15:36:02 2010 +0200
     1.2 +++ b/src/Tools/isac/Scripts/Tools.sml	Thu Aug 19 15:41:56 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4    (t as (Const(op0,t0) $ arg)) thy = 
     1.5    let 
     1.6      val t' = ((list2isalist HOLogic.realT) o vars) t;
     1.7 -    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
     1.8 +    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
     1.9    in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.10    | eval_var _ _ _ _ = raise GO_ON;
    1.11  (* 
    1.12 @@ -21,14 +21,14 @@
    1.13  > val (SOME(thmId,t')) = eval_var thmid op0 t;
    1.14  val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
    1.15    : (string * term) option
    1.16 -> Sign.string_of_term (sign_of thy) t';
    1.17 +> Syntax.string_of_term (thy2ctxt thy) t';
    1.18  val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
    1.19  *)
    1.20  fun eval_Length (thmid:string) (op_:string) 
    1.21    (t as (Const(op0,t0) $ arg)) thy = 
    1.22    let 
    1.23      val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
    1.24 -    val thmId = thmid^(Sign.string_of_term (sign_of thy) arg);
    1.25 +    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
    1.26    in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.27    | eval_Length _ _ _ _ = raise GO_ON;
    1.28  (*
    1.29 @@ -77,9 +77,9 @@
    1.30        let 
    1.31  	val t' = (nth (num_of_term t1) (isalist2list t2))
    1.32  	  handle _ => raise GO_ON; 
    1.33 -	val thmId = thmid^(Sign.string_of_term (sign_of thy) t1)^
    1.34 -	  "_"^(Sign.string_of_term (sign_of thy) t2)^
    1.35 -	  " = "^(Sign.string_of_term (sign_of thy) t');
    1.36 +	val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^
    1.37 +	  "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^
    1.38 +	  " = "^(Syntax.string_of_term (thy2ctxt thy) t');
    1.39        in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
    1.40    else raise GO_ON
    1.41  )