1.1 --- a/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Oct 02 15:14:51 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/DiophantEq.thy	Wed Oct 02 16:02:17 2019 +0200
     1.3 @@ -29,8 +29,8 @@
     1.4    where
     1.5  "diophant_equation e_e v_v = (
     1.6    Repeat (
     1.7 -    (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) @@
     1.8 -    (Try (Calculate ''PLUS'')) @@
     1.9 +    (Try (Rewrite_Inst [(''bdv'', v_v)] ''int_isolate_add'' )) #>
    1.10 +    (Try (Calculate ''PLUS'')) #>
    1.11      (Try (Calculate ''TIMES''))) e_e)"
    1.12  setup \<open>KEStore_Elems.add_mets
    1.13      [Specify.prep_met thy "met_test_diophant" [] Celem.e_metID