1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 21 12:26:08 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Tue Apr 21 15:42:50 2020 +0200
     1.3 @@ -877,7 +877,7 @@
     1.4  
     1.5  section \<open>A problem for simplification of rationals\<close>
     1.6  setup \<open>KEStore_Elems.add_pbts
     1.7 -  [(Specify.prep_pbt thy "pbl_simp_rat" [] Celem.e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_simp_rat" [] Spec.e_pblID
     1.9        (["rational","simplification"],
    1.10          [("#Given" ,["Term t_t"]),
    1.11            ("#Where" ,["t_t is_ratpolyexp"]),
    1.12 @@ -905,7 +905,7 @@
    1.13     Try (Rewrite_Set ''discard_parentheses1''))
    1.14     term)"
    1.15  setup \<open>KEStore_Elems.add_mets
    1.16 -    [Specify.prep_met thy "met_simp_rat" [] Celem.e_metID
    1.17 +    [Specify.prep_met thy "met_simp_rat" [] Spec.e_metID
    1.18        (["simplification","of_rationals"],
    1.19          [("#Given" ,["Term t_t"]),
    1.20            ("#Where" ,["t_t is_ratpolyexp"]),