1.1 --- a/src/Tools/isac/Knowledge/RootRatEq.thy	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/RootRatEq.thy	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -57,8 +57,8 @@
     1.4  
     1.5  fun eval_is_rootRatAddTerm_in _ _ (p as (Const (\<^const_name>\<open>is_rootRatAddTerm_in\<close>,_) $ t $ v)) _ =
     1.6      if is_rootRatAddTerm_in t v
     1.7 -    then SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
     1.8 -    else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
     1.9 +    then SOME ((UnparseC.term @{context} p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.10 +    else SOME ((UnparseC.term @{context} p) ^ " = True", HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.11    | eval_is_rootRatAddTerm_in _ _ _ _ = ((*tracing"### nichts matcht";*) NONE);
    1.12  \<close>
    1.13  calculation is_rootRatAddTerm_in = \<open>eval_is_rootRatAddTerm_in ""\<close>