1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 11:54:20 2021 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Thu Jun 10 12:23:57 2021 +0200
1.3 @@ -878,7 +878,7 @@
1.4
1.5 section \<open>A problem for simplification of rationals\<close>
1.6 setup \<open>KEStore_Elems.add_pbts
1.7 - [(Problem.prep_input thy "pbl_simp_rat" [] Problem.id_empty
1.8 + [(Problem.prep_input @{theory} "pbl_simp_rat" [] Problem.id_empty
1.9 (["rational", "simplification"],
1.10 [("#Given" ,["Term t_t"]),
1.11 ("#Where" ,["t_t is_ratpolyexp"]),
1.12 @@ -906,7 +906,7 @@
1.13 Try (Rewrite_Set ''discard_parentheses1''))
1.14 term)"
1.15 setup \<open>KEStore_Elems.add_mets
1.16 - [MethodC.prep_input thy "met_simp_rat" [] MethodC.id_empty
1.17 + [MethodC.prep_input @{theory} "met_simp_rat" [] MethodC.id_empty
1.18 (["simplification", "of_rationals"],
1.19 [("#Given" ,["Term t_t"]),
1.20 ("#Where" ,["t_t is_ratpolyexp"]),