src/Tools/isac/Knowledge/Rational.thy
changeset 60154 2ab0d1523731
parent 60017 cdcc5eba067b
child 60242 73ee61385493
     1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Wed Feb 03 15:21:12 2021 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Wed Feb 03 16:39:44 2021 +0100
     1.3 @@ -905,7 +905,7 @@
     1.4     Try (Rewrite_Set ''discard_parentheses1''))
     1.5     term)"
     1.6  setup \<open>KEStore_Elems.add_mets
     1.7 -    [Method.prep_input thy "met_simp_rat" [] Method.id_empty
     1.8 +    [MethodC.prep_input thy "met_simp_rat" [] MethodC.id_empty
     1.9        (["simplification", "of_rationals"],
    1.10          [("#Given" ,["Term t_t"]),
    1.11            ("#Where" ,["t_t is_ratpolyexp"]),