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