1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Apr 10 16:16:09 2020 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Fri Apr 10 18:32:36 2020 +0200
     1.3 @@ -43,9 +43,9 @@
     1.4  fun eval_is_ratpolyexp (thmid:string) _ 
     1.5  		       (t as (Const("Rational.is'_ratpolyexp", _) $ arg)) thy =
     1.6      if is_ratpolyexp arg
     1.7 -    then SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "", 
     1.8 +    then SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "", 
     1.9  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.10 -    else SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "", 
    1.11 +    else SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "", 
    1.12  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.13    | eval_is_ratpolyexp _ _ _ _ = NONE; 
    1.14  
    1.15 @@ -54,7 +54,7 @@
    1.16  		      (t as Const ("Rational.get_denominator", _) $
    1.17                (Const ("Rings.divide_class.divide", _) $ _(*num*) $
    1.18                  denom)) thy = 
    1.19 -      SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy denom) "", 
    1.20 +      SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy denom) "", 
    1.21  	            HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
    1.22    | eval_get_denominator _ _ _ _ = NONE; 
    1.23  
    1.24 @@ -63,7 +63,7 @@
    1.25        (t as Const ("Rational.get_numerator", _) $
    1.26            (Const ("Rings.divide_class.divide", _) $num
    1.27              $denom )) thy = 
    1.28 -    SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy num) "", 
    1.29 +    SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy num) "", 
    1.30  	    HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
    1.31    | eval_get_numerator _ _ _ _ = NONE; 
    1.32  \<close>
    1.33 @@ -132,7 +132,7 @@
    1.34    | monom_of_term vs (c, es) (Const ("Groups.times_class.times", _) $ m1 $ m2) =
    1.35      let val (c', es') = monom_of_term vs (c, es) m1
    1.36      in monom_of_term vs (c', es') m2 end
    1.37 -  | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term2str t)
    1.38 +  | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
    1.39  
    1.40  fun monoms_of_term vs (t as Const _) =
    1.41      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.42 @@ -144,7 +144,7 @@
    1.43      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.44    | monoms_of_term vs (Const ("Groups.plus_class.plus", _) $ ms1 $ ms2) =
    1.45      (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
    1.46 -  | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term2str t)
    1.47 +  | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
    1.48  
    1.49  (* convert a term to the internal representation of a multivariate polynomial;
    1.50    the conversion is quite liberal, see test --- fun poly_of_term ---:
    1.51 @@ -451,9 +451,9 @@
    1.52  fun eval_is_expanded (thmid:string) _ 
    1.53  		       (t as (Const("Rational.is'_expanded", _) $ arg)) thy = 
    1.54      if is_expanded arg
    1.55 -    then SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "", 
    1.56 +    then SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "", 
    1.57  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.58 -    else SOME (TermC.mk_thmid thmid (UnparseC.term_to_string''' thy arg) "", 
    1.59 +    else SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "", 
    1.60  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.61    | eval_is_expanded _ _ _ _ = NONE;
    1.62  \<close>
    1.63 @@ -491,7 +491,7 @@
    1.64        in
    1.65          case ropt of SOME ta => [(r, ta)]
    1.66  	      | NONE => ((*tracing 
    1.67 -	          ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*) []) 
    1.68 +	          ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
    1.69  			end
    1.70      else ((*tracing ("### locate_rule:  " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
    1.71    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";
    1.72 @@ -553,7 +553,7 @@
    1.73          case ropt of
    1.74            SOME ta => [(r, ta)]
    1.75  	      | NONE => 
    1.76 -	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term2str t ^ " = NONE");*)
    1.77 +	        ((*tracing ("### locate_rule:  rewrite " ^ ThmC_Def.id_of_thm r ^ " " ^ UnparseC.term t ^ " = NONE");*)
    1.78  	        []) end
    1.79      else ((*tracing ("### locate_rule:  " ^ ThmC_Def.id_of_thm r ^ " not mem rrls");*) [])
    1.80    | locate_rule _ _ _ _ _ _ = error "locate_rule: doesnt match rev-sets in istate";