diff -r b1f0389ca11f -r 73dc85c025ab src/Tools/isac/Knowledge/LinEq.thy
--- a/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 13:40:36 2014 +0100
+++ b/src/Tools/isac/Knowledge/LinEq.thy	Mon Jan 27 21:49:27 2014 +0100
@@ -140,7 +140,7 @@
   LinEq_prls, SOME "solve (e_e::bool, v_v)",
   [["LinEq","solve_lineq_equation"]]));
 *}
-setup {* KEStore_Elems.store_pbts
+setup {* KEStore_Elems.add_pbts
   [(prep_pbt thy "pbl_equ_univ_lin" [] e_pblID
       (["LINEAR", "univariate", "equation"],
         [("#Given" ,["equality e_e", "solveFor v_v"]),