1.1 --- a/src/Tools/isac/Knowledge/PolyMinus.thy	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyMinus.thy	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -134,18 +134,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.term2str p) ^ " = True",
     1.8 +		 SOME ((UnparseC.term p) ^ " = True",
     1.9  		       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.10 -	     else SOME ((UnparseC.term2str p) ^ " = False",
    1.11 +	     else SOME ((UnparseC.term p) ^ " = False",
    1.12  			HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.13  	 else (* -1 * -2 kleiner 0 *)
    1.14 -	     SOME ((UnparseC.term2str p) ^ " = False",
    1.15 +	     SOME ((UnparseC.term 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.term2str p) ^ " = True",
    1.20 +	     SOME ((UnparseC.term p) ^ " = True",
    1.21  		  HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.22 -	else SOME ((UnparseC.term2str p) ^ " = False",
    1.23 +	else SOME ((UnparseC.term 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 ("PolyMinus.ist'_monom",_) $ a)) _  =
    1.30      if ist_monom a  then 
    1.31 -	SOME ((UnparseC.term2str p) ^ " = True",
    1.32 +	SOME ((UnparseC.term p) ^ " = True",
    1.33  	      HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.34 -    else SOME ((UnparseC.term2str p) ^ " = False",
    1.35 +    else SOME ((UnparseC.term p) ^ " = False",
    1.36  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.37    | eval_ist_monom _ _ _ _ =  NONE;
    1.38