1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy	Thu Apr 09 12:03:14 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy	Thu Apr 09 17:13:17 2020 +0200
     1.3 @@ -72,7 +72,7 @@
     1.4  (*WN080222
     1.5  (*("new_c", ("Integrate.new'_c", eval_new_c "#new_c_"))*)
     1.6  fun eval_new_c _ _ (p as (Const ("Integrate.new'_c",_) $ t)) _ =
     1.7 -     SOME ((Rule.term2str p) ^ " = " ^ Rule.term2str (new_c p),
     1.8 +     SOME ((UnparseC.term2str p) ^ " = " ^ UnparseC.term2str (new_c p),
     1.9  	  Trueprop $ (mk_equality (p, new_c p)))
    1.10    | eval_new_c _ _ _ _ = NONE;
    1.11  *)
    1.12 @@ -86,7 +86,7 @@
    1.13  		     Const ("HOL.eq", T) $ lh $ rh => 
    1.14  		     Const ("HOL.eq", T) $ lh $ TermC.mk_add rh (new_c rh)
    1.15  		   | p => TermC.mk_add p (new_c p)
    1.16 -    in SOME ((Rule.term2str p) ^ " = " ^ Rule.term2str p',
    1.17 +    in SOME ((UnparseC.term2str p) ^ " = " ^ UnparseC.term2str p',
    1.18  	  HOLogic.Trueprop $ (TermC.mk_equality (p, p')))
    1.19      end
    1.20    | eval_add_new_c _ _ _ _ = NONE;
    1.21 @@ -96,9 +96,9 @@
    1.22  fun eval_is_f_x _ _(p as (Const ("Integrate.is'_f'_x", _)
    1.23  					   $ arg)) _ =
    1.24      if TermC.is_f_x arg
    1.25 -    then SOME ((Rule.term2str p) ^ " = True",
    1.26 +    then SOME ((UnparseC.term2str p) ^ " = True",
    1.27  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term True})))
    1.28 -    else SOME ((Rule.term2str p) ^ " = False",
    1.29 +    else SOME ((UnparseC.term2str p) ^ " = False",
    1.30  	       HOLogic.Trueprop $ (TermC.mk_equality (p, @{term False})))
    1.31    | eval_is_f_x _ _ _ _ = NONE;
    1.32  \<close>