diff -r fa8d902b60bc -r 2ab0d1523731 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Wed Feb 03 15:21:12 2021 +0100
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Wed Feb 03 16:39:44 2021 +0100
@@ -127,7 +127,7 @@
 
 (*-------------- methods------------------------------------------------------*)
 setup \<open>KEStore_Elems.add_mets
-    [Method.prep_input thy "met_eqlin" [] Method.id_empty
+    [MethodC.prep_input thy "met_eqlin" [] MethodC.id_empty
       (["LinEq"], [],
         {rew_ord' = "tless_true",rls' = Atools_erls,calc = [], srls = Rule_Set.empty, prls = Rule_Set.empty,
           crls = LinEq_crls, errpats = [], nrls = norm_Poly},
@@ -151,7 +151,7 @@
   in
     Or_to_List e_e)"
 setup \<open>KEStore_Elems.add_mets
-    [Method.prep_input thy "met_eq_lin" [] Method.id_empty
+    [MethodC.prep_input thy "met_eq_lin" [] MethodC.id_empty
       (["LinEq", "solve_lineq_equation"],
         [("#Given", ["equality e_e", "solveFor v_v"]),
           ("#Where", ["Not ((lhs e_e) is_polyrat_in v_v)", "((lhs e_e)  has_degree_in v_v) = 1"]),
@@ -160,7 +160,7 @@
           crls = LinEq_crls, errpats = [], nrls = norm_Poly},
         @{thm solve_linear_equation.simps})]
 \<close>
-ML \<open>Method.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
+ML \<open>MethodC.from_store' @{theory} ["LinEq", "solve_lineq_equation"];\<close>
 
 end