1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Sat Jun 22 14:34:06 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Sun Jun 23 14:23:09 2019 +0200
     1.3 @@ -196,13 +196,13 @@
     1.4  	       Rule.Thm ("rat_power", TermC.num_str @{thm rat_power})
     1.5  		(*"(?a / ?b) ^^^ ?n = ?a ^^^ ?n / ?b ^^^ ?n"*)
     1.6  	       ],
     1.7 -      scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
     1.8 +      scr = Rule.EmptyScr
     1.9        }),
    1.10  		Rule.Rls_ make_rat_poly_with_parentheses,
    1.11  		Rule.Rls_ cancel_p_rls,(*FIXME:cancel_p does NOT order sometimes*)
    1.12  		Rule.Rls_ rat_reduce_1
    1.13  		],
    1.14 -       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
    1.15 +       scr = Rule.EmptyScr
    1.16         };
    1.17  
    1.18  (*.for simplify_Integral adapted from 'norm_Rational'.*)
    1.19 @@ -217,7 +217,7 @@
    1.20  		Rule.Rls_ norm_Rational_rls_noadd_fractions,(* the main rls (#)   *)
    1.21  		Rule.Rls_ discard_parentheses1 (* mult only                       *)
    1.22  		],
    1.23 -       scr = Rule.Prog ((Thm.term_of o the o (TermC.parse thy)) "empty_script")
    1.24 +       scr = Rule.EmptyScr
    1.25         };
    1.26  
    1.27  (*.simplify terms before and after Integration such that