1.1 --- a/test/Tools/isac/Knowledge/poly.sml	Mon Jun 21 14:39:52 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Mon Jun 21 15:36:09 2021 +0200
     1.3 @@ -186,10 +186,10 @@
     1.4  "----------- rewrite_set_ has_degree_in Const ('Partial_Fractions', _) -------------------------";
     1.5  val thy = @{theory Partial_Fractions}
     1.6  val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
     1.7 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
     1.8 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
     1.9  
    1.10  val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
    1.11 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.12 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.13  
    1.14  "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
    1.15  "----------- eval_ for is_expanded_in, is_poly_in, has_degree_in -------------------------------";
    1.16 @@ -223,10 +223,10 @@
    1.17  
    1.18  val thy = @{theory Partial_Fractions}
    1.19  val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*x + x \<up> 2) has_degree_in x) = 2";
    1.20 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.21 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.22  
    1.23  val expr = (Thm.term_of o the o (TermC.parse thy)) "((-8 - 2*AA + AA \<up> 2) has_degree_in AA) = 2";
    1.24 -val SOME (Const ("HOL.True", _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.25 +val SOME (Const (\<^const_name>\<open>True\<close>, _), []) = rewrite_set_ thy false PolyEq_prls expr;
    1.26  
    1.27  "-------- investigate (new 2002) uniary minus -----------";
    1.28  "-------- investigate (new 2002) uniary minus -----------";
    1.29 @@ -244,11 +244,11 @@
    1.30  *** . . . Var ((x, 0), real)
    1.31  *)
    1.32  case t of
    1.33 -  Const ("HOL.Trueprop", _) $
    1.34 -    (Const ("HOL.eq", _) $ 
    1.35 -      (Const ("Groups.minus_class.minus", _) $ Const ("Groups.zero_class.zero", _) $ 
    1.36 +  Const (\<^const_name>\<open>Trueprop\<close>, _) $
    1.37 +    (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ 
    1.38 +      (Const (\<^const_name>\<open>minus\<close>, _) $ Const (\<^const_name>\<open>Groups.zero\<close>, _) $ 
    1.39          Var (("x", 0), _)) $
    1.40 -             (Const ("Groups.uminus_class.uminus", _) $ Var (("x", 0), _))) => ()
    1.41 +             (Const (\<^const_name>\<open>uminus\<close>, _) $ Var (("x", 0), _))) => ()
    1.42  | _ => error "internal representation of \"0 - ?x = - ?x\" changed";
    1.43  
    1.44  (*----------------------------------- vvvv --------------------------------------------*)
    1.45 @@ -279,7 +279,7 @@
    1.46  (**** -------------
    1.47  *** Free ( -x, real)*)
    1.48  case t of
    1.49 -  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
    1.50 +  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
    1.51  | _ => error "internal representation of \"-x\" changed";
    1.52  (*----------------------------------- vvvvv -------------------------------------------*)
    1.53  val t = (Thm.term_of o the o (TermC.parse thy)) "- x";
    1.54 @@ -287,7 +287,7 @@
    1.55  (**** -------------
    1.56  *** Free ( -x, real) !!!!!!!!!!!!!!!!!!!!!!!! is the same !!!*)
    1.57  case t of
    1.58 -  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
    1.59 +  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
    1.60  | _ => error "internal representation of \"- x\" changed";
    1.61  (*----------------------------------- vvvvvv ------------------------------------------*)
    1.62  val t = (Thm.term_of o the o (TermC.parse thy)) "-(x)";
    1.63 @@ -295,7 +295,7 @@
    1.64  (**** -------------
    1.65  *** Free ( -x, real)*)
    1.66  case t of
    1.67 -  Const ("Groups.uminus_class.uminus", _) $ Free ("x", _) => ()
    1.68 +  Const (\<^const_name>\<open>uminus\<close>, _) $ Free ("x", _) => ()
    1.69  | _ => error "internal representation of \"-(x)\" changed";
    1.70  
    1.71  "-------- check make_polynomial with simple terms -------";
    1.72 @@ -361,10 +361,10 @@
    1.73  "----- eval_is_multUnordered ---";
    1.74  val tm = TermC.str2term "(5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (-1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + -1 * (3 * x \<up> 5 * -1) +  (-48 * x \<up> 4 + 8))) is_multUnordered";
    1.75  case eval_is_multUnordered "testid" "" tm thy of
    1.76 -    SOME (_, Const ("HOL.Trueprop", _) $ 
    1.77 -                   (Const ("HOL.eq", _) $
    1.78 +    SOME (_, Const (\<^const_name>\<open>Trueprop\<close>, _) $ 
    1.79 +                   (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
    1.80                            (Const ("Poly.is_multUnordered", _) $ _) $ 
    1.81 -                          Const ("HOL.True", _))) => ()
    1.82 +                          Const (\<^const_name>\<open>True\<close>, _))) => ()
    1.83    | _ => error "poly.sml diff. eval_is_multUnordered";
    1.84  
    1.85  "----- rewrite_set_ STILL DIDN'T WORK";