diff -r a747d5643f99 -r 7be2ad0e4acb src/Tools/isac/Knowledge/DiophantEq.thy
--- a/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Feb 02 02:45:11 2014 +0100
+++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Sun Feb 02 03:09:40 2014 +0100
@@ -29,24 +29,6 @@
         e_rls, SOME "solve (e_e::bool, v_v::int)", [["LinEq","solve_lineq_equation"]]))] *}
 
 text {*method solving the usecase*}
-ML {*
-store_met
-(prep_met thy "met_test_diophant" [] e_metID
- (["Test","solve_diophant"]:metID,
-  [("#Given" ,["boolTestGiven e_e","intTestGiven (v_v::int)"]),
-  (*                                      TODO: drop ^^^^^*)
-   ("#Where" ,[]),
-   ("#Find"  ,["boolTestFind s_s"]) 
-  ],
-   {rew_ord' = "e_rew_ord", rls' = tval_rls, srls = e_rls,
-    prls = e_rls, calc = [], crls = tval_rls, errpats = [], nrls = Test_simplify},
- "Script Diophant_equation (e_e::bool) (v_v::int)=                  " ^
- "(Repeat                                                          " ^
- "    ((Try (Rewrite_Inst [(bdv,v_v::int)] int_isolate_add False)) @@" ^
- "     (Try (Calculate PLUS)) @@  " ^
- "     (Try (Calculate TIMES))) e_e::bool)"
- ))
-*}
 setup {* KEStore_Elems.add_mets
   [prep_met thy "met_test_diophant" [] e_metID
       (["Test","solve_diophant"]:metID,