1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Dec 14 14:20:25 2016 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Dec 18 16:27:41 2016 +0100
     1.3 @@ -886,7 +886,7 @@
     1.4  
     1.5  section {* A problem for simplification of rationals *}
     1.6  setup {* KEStore_Elems.add_pbts
     1.7 -  [(prep_pbt thy "pbl_simp_rat" [] e_pblID
     1.8 +  [(Specify.prep_pbt thy "pbl_simp_rat" [] e_pblID
     1.9        (["rational","simplification"],
    1.10          [("#Given" ,["Term t_t"]),
    1.11            ("#Where" ,["t_t is_ratpolyexp"]),
    1.12 @@ -898,7 +898,7 @@
    1.13  (*WN061025 this methods script is copied from (auto-generated) script
    1.14    of norm_Rational in order to ease repair on inform*)
    1.15  setup {* KEStore_Elems.add_mets
    1.16 -  [prep_met thy "met_simp_rat" [] e_metID
    1.17 +  [Specify.prep_met thy "met_simp_rat" [] e_metID
    1.18        (["simplification","of_rationals"],
    1.19          [("#Given" ,["Term t_t"]),
    1.20            ("#Where" ,["t_t is_ratpolyexp"]),