diff -r c988bdecd7be -r 1da53d1540fe src/Tools/isac/Knowledge/Simplify.thy
--- a/src/Tools/isac/Knowledge/Simplify.thy	Wed Dec 14 14:20:25 2016 +0100
+++ b/src/Tools/isac/Knowledge/Simplify.thy	Sun Dec 18 16:27:41 2016 +0100
@@ -29,12 +29,12 @@
 *}
 (** problems **)
 setup {* KEStore_Elems.add_pbts
-  [(prep_pbt thy "pbl_simp" [] e_pblID
+  [(Specify.prep_pbt thy "pbl_simp" [] e_pblID
       (["simplification"],
         [("#Given" ,["Term t_t"]),
           ("#Find"  ,["normalform n_n"])],
         append_rls "e_rls" e_rls [(*for preds in where_*)], SOME "Simplify t_t", [])),
-    (prep_pbt thy "pbl_vereinfache" [] e_pblID
+    (Specify.prep_pbt thy "pbl_vereinfache" [] e_pblID
       (["vereinfachen"],
         [("#Given", ["Term t_t"]),
           ("#Find", ["normalform n_n"])],
@@ -42,7 +42,7 @@
 
 (** methods **)
 setup {* KEStore_Elems.add_mets
-  [prep_met thy "met_tsimp" [] e_metID
+  [Specify.prep_met thy "met_tsimp" [] e_metID
 	    (["simplification"],
 	      [("#Given" ,["Term t_t"]),
 		      ("#Find"  ,["normalform n_n"])],