1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Wed Dec 05 10:21:35 2012 +0100
1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Wed Dec 05 15:29:36 2012 +0100
1.3 @@ -91,8 +91,8 @@
1.4 val denom2 = parseNEW ctxt "(z + -1 * (-1 / 4))::real" |> the;
1.5
1.6 val test = HOLogic.mk_binop "Groups.plus_class.plus"
1.7 - (HOLogic.mk_binop "Rings.inverse_class.divide" (A_var, denom1),
1.8 - HOLogic.mk_binop "Rings.inverse_class.divide" (B_var, denom2));
1.9 + (HOLogic.mk_binop "Fields.inverse_class.divide" (A_var, denom1),
1.10 + HOLogic.mk_binop "Fields.inverse_class.divide" (B_var, denom2));
1.11
1.12 if term2str test = "?A / (z + -1 * (1 / 2)) + ?B / (z + -1 * (-1 / 4))" then ()
1.13 else error "HOLogic.mk_binop broken ?";