1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -59,9 +59,9 @@
     1.4       eval_factors_from_solution ""))
     1.5    this code is limited (max 3 solutions) AND has too little checks *)
     1.6  fun eval_factors_from_solution (thmid:string) _
     1.7 -    (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) thy =
     1.8 +    (t as Const (\<^const_name>\<open>Partial_Fractions.factors_from_solution\<close>, _) $ sol) ctxt =
     1.9        let val prod = factors_from_solution sol
    1.10 -      in SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy prod) "",
    1.11 +      in SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt prod) "",
    1.12             HOLogic.Trueprop $ (TermC.mk_equality (t, prod)))
    1.13        end
    1.14    | eval_factors_from_solution _ _ _ _ = NONE;