test/Tools/isac/Knowledge/polyminus.sml
changeset 59488 10a9e97e77c3
parent 59395 862eb17f9e16
child 59582 23984b62804f
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Dec 14 20:53:15 2018 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Dec 20 18:02:25 2018 +0100
     1.3 @@ -341,9 +341,9 @@
     1.4  "Script ProbeScript (e_e::bool) (w_s::bool list) =\
     1.5  \ (let e_e = Take e_e;                             \
     1.6  \      e_e = Substitute w_s e_e                    \
     1.7 -\ in (Repeat((Try (Repeat (Calculate TIMES))) @@  \
     1.8 -\            (Try (Repeat (Calculate PLUS ))) @@  \
     1.9 -\            (Try (Repeat (Calculate MINUS))))) e_e)"
    1.10 +\ in (Repeat((Try (Repeat (Calculate ''TIMES''))) @@  \
    1.11 +\            (Try (Repeat (Calculate ''PLUS''))) @@  \
    1.12 +\            (Try (Repeat (Calculate ''MINUS''))))) e_e)"
    1.13  val sc = (inst_abs o Thm.term_of o the o (parse thy)) str;
    1.14  atomty sc;
    1.15