1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Mar 13 17:33:07 2019 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Mar 13 17:44:30 2019 +0100
     1.3 @@ -101,19 +101,6 @@
     1.4  ---> exception TERM raised (line 539 of "logic.ML"): Illegal fixed variable: "z"
     1.5  thus we need another fun var2free in termC.sml*)
     1.6  
     1.7 -"----------- eval_drop_questionmarks --------------------";
     1.8 -"----------- eval_drop_questionmarks --------------------";
     1.9 -"----------- eval_drop_questionmarks --------------------";
    1.10 -if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))"
    1.11 -then () else error "test setup (ctxt!) probably changed";
    1.12 -
    1.13 -val t = Const ("Partial_Fractions.drop_questionmarks", HOLogic.realT --> HOLogic.realT) $ test;
    1.14 -
    1.15 -val SOME (_, t') = eval_drop_questionmarks "drop_questionmarks" 0 t @{theory Isac};
    1.16 -if term2str t' = "drop_questionmarks (?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))) =" ^
    1.17 -  "\nA / (z + -1 * (1 / 2)) + B / (z + -1 * (-1 / 4))"
    1.18 -then () else error "eval_drop_questionmarks broken";
    1.19 -
    1.20  "----------- = me for met_partial_fraction --------------";
    1.21  "----------- = me for met_partial_fraction --------------";
    1.22  "----------- = me for met_partial_fraction --------------";