diff -r f8852715be0d -r 7701598a2182 src/Tools/isac/Knowledge/Rational.thy
--- a/src/Tools/isac/Knowledge/Rational.thy	Sun Jul 18 21:19:25 2021 +0200
+++ b/src/Tools/isac/Knowledge/Rational.thy	Mon Jul 19 15:34:54 2021 +0200
@@ -41,7 +41,7 @@
 
 (*("is_ratpolyexp", ("Rational.is_ratpolyexp", eval_is_ratpolyexp ""))*)
 fun eval_is_ratpolyexp (thmid:string) _ 
-		       (t as (Const("Rational.is_ratpolyexp", _) $ arg)) thy =
+		       (t as (Const (\<^const_name>\<open>Rational.is_ratpolyexp\<close>, _) $ arg)) thy =
     if is_ratpolyexp arg
     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))
@@ -51,7 +51,7 @@
 
 (*("get_denominator", ("Rational.get_denominator", eval_get_denominator ""))*)
 fun eval_get_denominator (thmid:string) _ 
-		      (t as Const ("Rational.get_denominator", _) $
+		      (t as Const (\<^const_name>\<open>Rational.get_denominator\<close>, _) $
               (Const (\<^const_name>\<open>divide\<close>, _) $ _(*num*) $
                 denom)) thy = 
       SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy denom) "", 
@@ -60,7 +60,7 @@
 
 (*("get_numerator", ("Rational.get_numerator", eval_get_numerator ""))*)
 fun eval_get_numerator (thmid:string) _ 
-      (t as Const ("Rational.get_numerator", _) $
+      (t as Const (\<^const_name>\<open>Rational.get_numerator\<close>, _) $
           (Const (\<^const_name>\<open>divide\<close>, _) $num
             $denom )) thy = 
     SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy num) "", 
@@ -123,17 +123,17 @@
 ML \<open>
 fun monom_of_term vs (c, es) (t as Const _) =
     (c, list_update es (find_index (curry op = t) vs) 1)
-  | monom_of_term _ (c, es) (t as (Const ("Num.numeral_class.numeral", _) $ _)) =
+  | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
-  | monom_of_term _ (c, es) (t as (Const ("Groups.uminus_class.uminus", _) $ _)) =
+  | monom_of_term _ (c, es) (t as (Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
     (t |> HOLogic.dest_number |> snd |> curry op * c, es) (*several numerals in one monom*)
   | monom_of_term  vs (c, es) (t as Free _) =
     (c, list_update es (find_index (curry op = t) vs) 1)
-  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
-      (e as Const ("Num.numeral_class.numeral", _) $ _)) =
+  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
+      (e as Const (\<^const_name>\<open>numeral\<close>, _) $ _)) =
     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
-  | monom_of_term  vs (c, es) (Const ("Transcendental.powr", _) $ (b as Free _) $
-      (e as Const ("Groups.uminus_class.uminus", _) $ _)) =
+  | monom_of_term  vs (c, es) (Const (\<^const_name>\<open>Transcendental.powr\<close>, _) $ (b as Free _) $
+      (e as Const (\<^const_name>\<open>uminus\<close>, _) $ _)) =
     (c, list_update es (find_index (curry op = b) vs) (e |> HOLogic.dest_number |> snd))
 
   | monom_of_term vs (c, es) (Const (\<^const_name>\<open>times\<close>, _) $ m1 $ m2) =
@@ -144,9 +144,9 @@
 (*-------v------*)
 fun monoms_of_term vs (t as Const _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
-  | monoms_of_term vs (t as Const ("Num.numeral_class.numeral", _) $ _) =
+  | monoms_of_term vs (t as Const (\<^const_name>\<open>numeral\<close>, _) $ _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
-  | monoms_of_term vs (t as Const ("Groups.uminus_class.uminus", _) $ _) =
+  | monoms_of_term vs (t as Const (\<^const_name>\<open>uminus\<close>, _) $ _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
   | monoms_of_term vs (t as Free _) =
     [monom_of_term  vs (1, replicate (length vs) 0) t]
@@ -191,7 +191,7 @@
   | term_of_es baseT expT (_ :: vs) (0 :: es) = [] @ term_of_es baseT expT vs es
   | term_of_es baseT expT (v :: vs) (1 :: es) = v :: term_of_es baseT expT vs es
   | term_of_es baseT expT (v :: vs) (e :: es) =
-    Const ("Transcendental.powr", [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
+    Const (\<^const_name>\<open>Transcendental.powr\<close>, [baseT, expT] ---> baseT) $ v $ (HOLogic.mk_number expT e)
     :: term_of_es baseT expT vs es
   | term_of_es _ _ _ _ = raise ERROR "term_of_es: length vs <> length es"
 
@@ -215,8 +215,8 @@
 subsection \<open>Apply gcd_poly for cancelling and adding fractions as terms\<close>
 ML \<open>
 fun mk_noteq_0 baseT t = 
-  Const ("HOL.Not", HOLogic.boolT --> HOLogic.boolT) $ 
-    (Const ("HOL.eq", [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
+  Const (\<^const_name>\<open>Not\<close>, HOLogic.boolT --> HOLogic.boolT) $ 
+    (Const (\<^const_name>\<open>HOL.eq\<close>, [baseT, baseT] ---> HOLogic.boolT) $ t $ HOLogic.mk_number HOLogic.realT 0)
 
 fun mk_asms baseT ts =
   let val as' = filter_out TermC.is_num ts (* asm like "2 ~= 0" is needless *)
@@ -464,7 +464,7 @@
 
 (*("is_expanded", ("Rational.is_expanded", eval_is_expanded ""))*)
 fun eval_is_expanded (thmid:string) _ 
-		       (t as (Const("Rational.is_expanded", _) $ arg)) thy = 
+		       (t as (Const (\<^const_name>\<open>Rational.is_expanded\<close>, _) $ arg)) thy = 
     if is_expanded arg
     then SOME (TermC.mk_thmid thmid (UnparseC.term_in_thy thy arg) "", 
 	         HOLogic.Trueprop $ (TermC.mk_equality (t, @{term True})))