1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml Fri Oct 12 16:03:07 2012 +0200
1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml Fri Oct 12 17:06:58 2012 +0200
1.3 @@ -74,7 +74,7 @@
1.4 "----------- fun factors_from_solution ------------------";
1.5 "----------- fun factors_from_solution ------------------";
1.6 "----------- fun factors_from_solution ------------------";
1.7 -val ctxt = ProofContext.init_global @{theory Isac};
1.8 +val ctxt = Proof_Context.init_global @{theory Isac};
1.9 val SOME t = parseNEW ctxt "factors_from_solution [(z::real) = 1 / 2, z = -1 / 4]";
1.10 val SOME (_, t') = eval_factors_from_solution "" 0 t thy;
1.11 if term2str t' =