1.1 --- a/test/Tools/isac/Knowledge/rational-2.sml	Mon Jul 19 15:34:54 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational-2.sml	Mon Jul 19 17:29:35 2021 +0200
     1.3 @@ -453,7 +453,7 @@
     1.4  
     1.5  "~~~~~ fun monom_of_term , args:"; val (vs, (c, es), (Const (id, _))) =
     1.6    (vs, (1, replicate (length vs) 0), t);
     1.7 -case vs of [Const ("Partial_Fractions.AA", _), Const ("Partial_Fractions.BB", _)] =>
     1.8 +case vs of [Const (\<^const_name>\<open>AA\<close>, _), Const (\<^const_name>\<open>BB\<close>, _)] =>
     1.9    if c = 1 andalso id = "Partial_Fractions.AA"
    1.10    then () else error "monom_of_term Const changed 1"
    1.11  | _ => error "monom_of_term Const changed 2";
    1.12 @@ -463,12 +463,12 @@
    1.13  "----------- fun cancel_p with Const AA --------------------------------------------------------";
    1.14  val thy = @{theory Partial_Fractions};
    1.15  val ctxt = Proof_Context.init_global @{theory}
    1.16 -val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const ("Free ("AA", "real") *)
    1.17 +val SOME t = TermC.parseNEW ctxt "2 * AA / 2"; (* Const (\<^const_name>\<open>AA\<close>, "real") *)
    1.18  
    1.19  val SOME (t', _) = rewrite_set_ thy true cancel_p t;
    1.20  case t' of
    1.21 -  Const ("Rings.divide_class.divide", _) $ Const ("Partial_Fractions.AA", _) $
    1.22 -    Const ("Groups.one_class.one", _) => ()
    1.23 +  Const (\<^const_name>\<open>divide\<close>, _) $ Const (\<^const_name>\<open>AA\<close>, _) $
    1.24 +    Const (\<^const_name>\<open>one_class.one\<close>, _) => ()
    1.25  | _ => error "WRONG rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA changed";
    1.26  
    1.27  "~~~~~ fun cancel_p , args:"; val (t) = (t);
    1.28 @@ -479,7 +479,7 @@
    1.29  then () else error "check_fraction (2 * AA / 2) changed";
    1.30          val vs = TermC.vars_of t;
    1.31  case vs of
    1.32 -  [Const ("Partial_Fractions.AA", _)] => ()
    1.33 +  [Const (\<^const_name>\<open>AA\<close>, _)] => ()
    1.34  | _ => error "rewrite_set_ cancel_p (2 * AA / 2) \<longrightarrow> AA/1  changed";
    1.35  
    1.36