1.1 --- a/src/Tools/isac/Knowledge/Rational.thy Mon Apr 13 13:13:07 2020 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Rational.thy Mon Apr 13 13:27:55 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_thy thy arg) "",
1.8 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.9 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.10 - else SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "",
1.11 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_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_thy thy denom) "",
1.20 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_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_thy thy num) "",
1.29 + SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "",
1.30 HOLogic.Trueprop $ (TermC.mk_equality (t, num)))
1.31 | eval_get_numerator _ _ _ _ = NONE;
1.32 \<close>
1.33 @@ -451,9 +451,9 @@
1.34 fun eval_is_expanded (thmid:string) _
1.35 (t as (Const("Rational.is'_expanded", _) $ arg)) thy =
1.36 if is_expanded arg
1.37 - then SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "",
1.38 + then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.39 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
1.40 - else SOME (TermC.mk_thmid thmid (UnparseC.term_thy thy arg) "",
1.41 + else SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "",
1.42 HOLogic.Trueprop $ (TermC.mk_equality (t, @{term False})))
1.43 | eval_is_expanded _ _ _ _ = NONE;
1.44 \<close>