1.1 --- a/src/Tools/isac/Knowledge/Rational.thy	Sun Jul 31 13:45:20 2022 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy	Sun Jul 31 16:35:33 2022 +0200
     1.3 @@ -41,11 +41,11 @@
     1.4  
     1.5  (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
     1.6  fun eval_is_ratpolyexp (thmid:string) _ 
     1.7 -		       (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
     1.8 +		       (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) ctxt =
     1.9      if is_ratpolyexp arg
    1.10 -    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
    1.11 +    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
    1.12  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.13 -    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
    1.14 +    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
    1.15  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.16    | eval_is_ratpolyexp _ _ _ _ = NONE; 
    1.17  
    1.18 @@ -53,8 +53,8 @@
    1.19  fun eval_get_denominator (thmid:string) _ 
    1.20  		      (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
    1.21                (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
    1.22 -                denom)) thy = 
    1.23 -      SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", 
    1.24 +                denom)) ctxt = 
    1.25 +      SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt denom) "", 
    1.26  	            HOLogic.Trueprop $ (TermC.mk_equality (t, denom)))
    1.27    | eval_get_denominator _ _ _ _ = NONE; 
    1.28  
    1.29 @@ -62,8 +62,8 @@
    1.30  fun eval_get_numerator (thmid:string) _ 
    1.31        (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
    1.32            (Const (\<^const_name>\<open>divide\<close>, _) $num
    1.33 -            $denom )) thy = 
    1.34 -    SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "", 
    1.35 +            $denom )) ctxt = 
    1.36 +    SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt num) "", 
    1.37  	    HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
    1.38    | eval_get_numerator _ _ _ _ = NONE; 
    1.39  \<close>
    1.40 @@ -454,11 +454,11 @@
    1.41  
    1.42  (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
    1.43  fun eval_is_expanded (thmid:string) _ 
    1.44 -		       (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy = 
    1.45 +		       (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) ctxt = 
    1.46      if is_expanded arg
    1.47 -    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
    1.48 +    then SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
    1.49  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
    1.50 -    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
    1.51 +    else SOME (TermC.mk_thmid thmid (UnparseC.term_in_ctxt ctxt arg) "", 
    1.52  	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
    1.53    | eval_is_expanded _ _ _ _ = NONE;
    1.54  \<close>