diff -r a28b5fc129b7 -r 22235e4dbe5f src/Tools/isac/Scripts/Tools.sml
--- a/src/Tools/isac/Scripts/Tools.sml	Wed Aug 25 15:15:01 2010 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,113 +0,0 @@
-(* = Tools.ML
-   +++ outcommented tests *)
-
-
-fun eval_var (thmid:string) (op_:string) 
-  (t as (Const(op0,t0) $ arg)) thy = 
-  let 
-    val t' = ((list2isalist HOLogic.realT) o vars) t;
-    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
-  in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
-  | eval_var _ _ _ _ = raise GO_ON;
-(* 
-> val t = (term_of o the o (parse thy)) "Var (A=a*(b::real))";
-> val op_ = "Var";
-> val eval_fn = the (assoc (!eval_list, op_));
-> get_pair op_ eval_fn t;
-> val (t as (Const(op0,t0) $ arg)) = t;
-> eval_fn op0 t; 
-
-> val thmid = "#Var_";
-> val (SOME(thmId,t')) = eval_var thmid op0 t;
-val it = SOME ("#Var_(A::real) = (a::real) * (b::real)",Const # $ (# $ #))
-  : (string * term) option
-> Syntax.string_of_term (thy2ctxt thy) t';
-val it = "Var ((A::real) = (a::real) * (b::real)) = [A, a, b]" : string
-*)
-fun eval_Length (thmid:string) (op_:string) 
-  (t as (Const(op0,t0) $ arg)) thy = 
-  let 
-    val t' = ((term_of_num HOLogic.realT) o length o isalist2list) arg;
-    val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) arg);
-  in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
-  | eval_Length _ _ _ _ = raise GO_ON;
-(*
-> val thmid = "#Length_"; val op_ = "Length";
-> val s = "Length [A = a * b, a // #2 = #2]";
-> val (t as (Const(op0,t0) $ arg)) = (term_of o the o (parse thy)) s;
-> val (SOME (id,t')) = eval_Length thmid op_ t;
-val id = "#Length_[A = a * b, a // #2 = #2]" : string
-val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
-val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
----------------------------------------------
-> val thmid = "#Length_"; val op_ = "Length";
-> val s = 
- "if #1 < Length [A = a * b, a // #2 = #2]       \
- \then make_fun (R, [make, function], no_met) A a_ [A = a * b, a // #2 = #2]\
- \else hd [A = a * b, a // #2 = #2]";
-
-> (cterm_of thy) t';
-> val t = (term_of o the o (parse thy)) s;
-> val eval_fn = the (assoc (!eval_list, op_));
-> val (SOME(_,t')) = get_pair op_ eval_fn t;
-val t' = Const ("Trueprop","bool => prop") $ (Const # $ (# $ #) $ Free (#,#))
-val it = "Length [A = a * b, a // #2 = #2] = #2" : cterm
-
-> val ct = (the o (parse thy)) s;
-> val (SOME(_,thm)) = get_calculation thy (op_, eval_fn) ct;
-val thm = "Length [A = a * b, a // #2 = #2] = #2" [[ Free ( #2, real) !!!]]
-> rewrite_ thy tless_true e_rls false thm ct;
-("if #1 < #2
-  then make_fun (R, [make, function], no_met)
-       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
- []) : (cterm * cterm list) option
-> val ct = (the o (parse thy)) s;
-> rewrite_set_ thy e_rls false eval_script ct;
-("if #1 < #2
-  then make_fun (R, [make, function], no_met)
-       A a_ [A = a * b, a // #2 = #2] else hd [A = a * b, a // #2 = #2]",
- []) : (cterm * cterm list) option
-*)
-
-fun eval_Nth (thmid:string) (op_:string) (t as 
-	       (Const (op0,t0) $ t1 $ t2 )) thy =
-(writeln"@@@ eval_Nth";
-  if is_num t1 andalso is_list t2
-    then
-      let 
-	val t' = (nth (num_of_term t1) (isalist2list t2))
-	  handle _ => raise GO_ON; 
-	val thmId = thmid^(Syntax.string_of_term (thy2ctxt thy) t1)^
-	  "_"^(Syntax.string_of_term (thy2ctxt thy) t2)^
-	  " = "^(Syntax.string_of_term (thy2ctxt thy) t');
-      in SOME (thmId, Trueprop $ (mk_equality (t,t'))) end
-  else raise GO_ON
-)
-  | eval_Nth _ _ _ _ = raise GO_ON;
-(*
-> val thmid = "#Nth_"; val op_ = "Nth";
-> val s = "Nth #2 [A = a * b, a // #2 = #2]";
-> val t = (term_of o the o (parse thy)) s;
-> eval_Nth thmid op_ t;
-
-> val eval_fn = the (assoc (!eval_list, op_));
-> val (SOME(id,t')) = get_pair op_ eval_fn t;
-> (cterm_of thy) t';
-val it = "Nth #2 [A = a * b, a // #2 = #2] = (a // #2 = #2)"
-*)
-
-
-(*17.6.00: calc_list instead eval_list*)
-eval_list:= overwritel (! eval_list,
-            [("Var",eval_var "#Var_"),
-	     ("Length",eval_Length "#Length_"),
-	     ("Nth",eval_Nth "#Nth_")
-	     ]);
-(*17.6.00: association list for calculate_, calculate*)
-calc_list:= overwritel (! calc_list,
-            [
-	     ("Var"   ,("Var",eval_var "#Var_")),
-	     ("Length",("Length",eval_Length "#Length_")),
-	     ("Nth"   ,("Nth",eval_Nth "#Nth_"))
-	     ]);
-