diff -r 8cba439d0454 -r 68883c046963 src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Tue Apr 21 12:26:08 2020 +0200
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Tue Apr 21 15:42:50 2020 +0200
@@ -114,7 +114,7 @@
 (*----------------------------- problem types --------------------------------*)
 (* ---------linear----------- *)
 setup \<open>KEStore_Elems.add_pbts
-  [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Celem.e_pblID
+  [(Specify.prep_pbt thy "pbl_equ_univ_lin" [] Spec.e_pblID
       (["LINEAR", "univariate", "equation"],
         [("#Given" ,["equality e_e", "solveFor v_v"]),
           ("#Where" ,["HOL.False", (*WN0509 just detected: this pbl can never be used?!?*)
@@ -127,7 +127,7 @@
 
 (*-------------- methods------------------------------------------------------*)
 setup \<open>KEStore_Elems.add_mets
-    [Specify.prep_met thy "met_eqlin" [] Celem.e_metID
+    [Specify.prep_met thy "met_eqlin" [] Spec.e_metID
       (["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
-    [Specify.prep_met thy "met_eq_lin" [] Celem.e_metID
+    [Specify.prep_met thy "met_eq_lin" [] Spec.e_metID
       (["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"]),