1.1 --- a/test/Tools/isac/OLDTESTS/root-equ.sml	Mon May 18 11:48:27 2020 +0200
     1.2 +++ b/test/Tools/isac/OLDTESTS/root-equ.sml	Mon May 18 11:58:55 2020 +0200
     1.3 @@ -115,9 +115,6 @@
     1.4  val chkpbl = map (the o (parse thy)) (given @ where_ @ find @ with_);
     1.5  val givens = map (the o (parse thy)) given;
     1.6  parseold thy "L = {bdv. || ((%x. l) bdv) - ((%x. r) bdv) || < apx}";
     1.7 -(* 31.1.00 
     1.8 -val tag__forms = chktyps thy (formals, givens);
     1.9 -map ((atomty) o Thm.term_of) tag__forms;       *)
    1.10  
    1.11  " --- subproblem 2: linear-equation --- ";
    1.12  val origin = ["x + 4 = (0::real)","x::real"];
    1.13 @@ -131,10 +128,6 @@
    1.14  val chkpbl = map (the o (parseold thy)) (given @ where_ @ find @ with_);
    1.15  val givens = map (the o (parse thy)) given;
    1.16  
    1.17 -val tag__forms = chktyps thy (formals, givens);
    1.18 -map ((atomty) o Thm.term_of) tag__forms;
    1.19 -
    1.20 -
    1.21  
    1.22  " _________________ rewrite_ x+4_________________ ";
    1.23  " _________________ rewrite_ x+4_________________ ";