1.1 --- a/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jun 10 12:23:57 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/EqSystem.thy	Thu Jun 10 12:48:50 2021 +0200
     1.3 @@ -49,8 +49,6 @@
     1.4      works for lists of any length, interestingly !?!*)
     1.5  
     1.6  ML \<open>
     1.7 -val thy = @{theory};
     1.8 -
     1.9  (** eval functions **)
    1.10  
    1.11  (*certain variables of a given list occur _all_ in a term
    1.12 @@ -163,7 +161,7 @@
    1.13  end;
    1.14  (**)
    1.15  Rewrite_Ord.rew_ord' := overwritel (! Rewrite_Ord.rew_ord',
    1.16 -[("ord_simplify_System", ord_simplify_System false thy)
    1.17 +[("ord_simplify_System", ord_simplify_System false \<^theory>)
    1.18   ]);
    1.19  \<close>
    1.20  ML \<open>
    1.21 @@ -332,7 +330,7 @@
    1.22  val order_system = 
    1.23      Rule_Def.Repeat {id="order_system", preconds = [], 
    1.24  	 rew_ord = ("ord_simplify_System", 
    1.25 -		    ord_simplify_System false thy), 
    1.26 +		    ord_simplify_System false \<^theory>), 
    1.27  	 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
    1.28  	 rules = [Rule.Thm ("order_system_NxN", ThmC.numerals_to_Free @{thm order_system_NxN})
    1.29  		  ],