1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Fri Feb 03 15:26:19 2023 +0100
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sat Feb 04 09:47:27 2023 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4    | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
     1.5      let val (c', es') = monom_of_term vs (c, es) m1
     1.6      in monom_of_term vs (c', es') m2 end
     1.7 -  | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term t)
     1.8 +  | monom_of_term _ _ t = raise ERROR ("poly malformed 1 with " ^ UnparseC.term_in_ctxt @{context} t)
     1.9  
    1.10  (*-------v------*)
    1.11  fun monoms_of_term vs (t as Const (\<^const_name>\<open>zero_class.zero\<close>, _)) =
    1.12 @@ -160,7 +160,7 @@
    1.13      [monom_of_term  vs (1, replicate (length vs) 0) t]
    1.14    | monoms_of_term vs (Const (\<^const_name>\<open>plus\<close>, _) $ ms1 $ ms2) =
    1.15      (monoms_of_term vs ms1) @ (monoms_of_term vs ms2)
    1.16 -  | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term t)
    1.17 +  | monoms_of_term _ t = raise ERROR ("poly malformed 2 with " ^ UnparseC.term_in_ctxt @{context} t)
    1.18  
    1.19  (* convert a term to the internal representation of a multivariate polynomial;
    1.20    the conversion is quite liberal, see test --- fun poly_of_term ---:
    1.21 @@ -497,7 +497,7 @@
    1.22        in
    1.23          case ropt of SOME ta => [(r, ta)]
    1.24  	      | NONE => ((*tracing 
    1.25 -	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*) []) 
    1.26 +	          ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term_in_ctxt @{context} t ^ " = NONE");*) []) 
    1.27  			end
    1.28      else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
    1.29    | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";
    1.30 @@ -561,7 +561,7 @@
    1.31          case ropt of
    1.32            SOME ta => [(r, ta)]
    1.33  	      | NONE => 
    1.34 -	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term t ^ " = NONE");*)
    1.35 +	        ((*tracing ("### locate_rule:  rewrite " ^ Rule.thm_id r ^ " " ^ UnparseC.term_in_ctxt @{context} t ^ " = NONE");*)
    1.36  	        []) end
    1.37      else ((*tracing ("### locate_rule:  " ^ Rule.thm_id r ^ " not mem rrls");*) [])
    1.38    | locate_rule _ _ _ _ _ _ = raise ERROR "locate_rule: doesnt match rev-sets in istate";