1.1 --- a/src/Tools/isac/Knowledge/Poly.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Poly.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -177,7 +177,6 @@
     1.4  
     1.5  subsection \<open>auxiliary functions\<close>
     1.6  ML \<open>
     1.7 -val thy = @{theory};
     1.8  val poly_consts =
     1.9    ["Groups.plus_class.plus", "Groups.minus_class.minus",
    1.10    "Rings.divide_class.divide", "Groups.times_class.times",
    1.11 @@ -512,7 +511,7 @@
    1.12  end;(*local*)
    1.13  
    1.14  Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord', (* TODO: make analogous to KEStore_Elems.add_mets *)
    1.15 -[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false thy)]);
    1.16 +[("termlessI", termlessI), ("ord_make_polynomial", ord_make_polynomial false \<^theory>)]);
    1.17  \<close>
    1.18  
    1.19  subsection \<open>predicates\<close>
    1.20 @@ -1009,7 +1008,7 @@
    1.21    (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
    1.22  val order_add_mult = 
    1.23    Rule_Def.Repeat{id = "order_add_mult", preconds = [], 
    1.24 -      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
    1.25 +      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
    1.26        erls = Rule_Set.empty,srls = Rule_Set.Empty,
    1.27        calc = [], errpatts = [],
    1.28        rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
    1.29 @@ -1029,7 +1028,7 @@
    1.30    (total-degree-)ordering of monoms NOT possible with size_of_term GIVEN*)
    1.31  val order_mult = 
    1.32    Rule_Def.Repeat{id = "order_mult", preconds = [], 
    1.33 -      rew_ord = ("ord_make_polynomial",ord_make_polynomial false thy),
    1.34 +      rew_ord = ("ord_make_polynomial",ord_make_polynomial false \<^theory>),
    1.35        erls = Rule_Set.empty,srls = Rule_Set.Empty,
    1.36        calc = [], errpatts = [],
    1.37        rules = [Rule.Thm ("mult.commute",ThmC.numerals_to_Free @{thm mult.commute}),
    1.38 @@ -1054,8 +1053,8 @@
    1.39  	  prepat = 
    1.40            (* ?p matched with the current term gives an environment,
    1.41               which evaluates (the instantiated) "?p is_multUnordered" to true *)
    1.42 -	  [([TermC.parse_patt thy "?p is_multUnordered"], 
    1.43 -             TermC.parse_patt thy "?p :: real")],
    1.44 +	  [([TermC.parse_patt \<^theory> "?p is_multUnordered"], 
    1.45 +             TermC.parse_patt \<^theory> "?p :: real")],
    1.46  	  rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
    1.47  	  erls = Rule_Set.append_rules "Rule_Set.empty-is_multUnordered" Rule_Set.empty
    1.48  			    [Rule.Eval ("Poly.is_multUnordered",