1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Sat Feb 04 16:49:08 2023 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Sat Feb 04 17:00:25 2023 +0100
     1.3 @@ -144,18 +144,18 @@
     1.4      if TermC.is_num b then
     1.5    	  if TermC.is_num a then (*123 kleiner 32 = True !!!*)
     1.6    	    if TermC.num_of_term a < TermC.num_of_term b then 
     1.7 -  		    SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True", 
     1.8 +  		    SOME ((UnparseC.term @{context} p) ^ " = True", 
     1.9              HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.10 -  	    else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
    1.11 +  	    else SOME ((UnparseC.term @{context} p) ^ " = False",
    1.12    			  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.13    	  else (* -1 * -2 kleiner 0 *)
    1.14 -  	    SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
    1.15 +  	    SOME ((UnparseC.term @{context} p) ^ " = False",
    1.16    		    HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.17      else
    1.18      	if identifier a < identifier b then 
    1.19 -    	  SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
    1.20 +    	  SOME ((UnparseC.term @{context} p) ^ " = True",
    1.21      		  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.22 -    	else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
    1.23 +    	else SOME ((UnparseC.term @{context} p) ^ " = False",
    1.24      		HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.25    | eval_kleiner _ _ _ _ =  NONE;
    1.26  
    1.27 @@ -173,9 +173,9 @@
    1.28  (*("ist_monom", ("PolyMinus.ist_monom", eval_ist_monom ""))*)
    1.29  fun eval_ist_monom _ _ (p as (Const (\<^const_name>\<open>PolyMinus.ist_monom\<close>,_) $ a)) _  =
    1.30      if ist_monom a  then 
    1.31 -	SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = True",
    1.32 +	SOME ((UnparseC.term @{context} p) ^ " = True",
    1.33  	      HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.34 -    else SOME ((UnparseC.term_in_ctxt @{context} p) ^ " = False",
    1.35 +    else SOME ((UnparseC.term @{context} p) ^ " = False",
    1.36  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.37    | eval_ist_monom _ _ _ _ =  NONE;
    1.38