test/Tools/isac/Interpret/script.sml
changeset 59395 862eb17f9e16
parent 59279 255c853ea2f0
child 59497 8952c43fdce3
     1.1 --- a/test/Tools/isac/Interpret/script.sml	Wed Mar 07 14:20:33 2018 +0100
     1.2 +++ b/test/Tools/isac/Interpret/script.sml	Thu Mar 08 07:28:17 2018 +0100
     1.3 @@ -39,7 +39,7 @@
     1.4  "       (M1__M1::bool) = ((Substitute [v_v = 0])) q___q              " ^
     1.5  " in True)";
     1.6  
     1.7 -val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
     1.8 +val sc' = (inst_abs o Thm.term_of o the o (parse thy)) str;
     1.9  
    1.10  val str = (*#2#*)
    1.11  "Script BiegelinieScript                                             " ^ 
    1.12 @@ -80,7 +80,7 @@
    1.13  " in True)"
    1.14  ;
    1.15  
    1.16 -val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
    1.17 +val sc' = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.18  atomty sc';
    1.19  
    1.20  val {scr = Prog sc,...} = get_met ["IntegrierenUndKonstanteBestimmen"];
    1.21 @@ -104,7 +104,7 @@
    1.22  "        M1__M1        = Substitute [e1__e1] M1__M1                  " ^
    1.23  " in True)"
    1.24  ;
    1.25 -val sc' = ((inst_abs thy) o Thm.term_of o the o (parse thy)) str;
    1.26 +val sc' = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.27  atomty sc';
    1.28  
    1.29  val str = (*Substitute @@ Substitute does NOT work???*)