1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Mon Mar 21 00:32:53 2011 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Mon Apr 04 11:05:07 2011 +0200
     1.3 @@ -26,8 +26,15 @@
     1.4  "----------- rewriting for usecase1 ---------------------";
     1.5  "----------- rewriting for usecase1 ---------------------";
     1.6  "----------- rewriting for usecase1 ---------------------";
     1.7 -val subst = [(parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int")];
     1.8 -val t = parseNEW ctxt "xxx + 111 = abc + (123::int)";
     1.9 +val subst = let
    1.10 +      val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");
    1.11 +    in case pair of
    1.12 +        (SOME r, SOME s) => [(r,s)]
    1.13 +      | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
    1.14 +    end;
    1.15 +val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
    1.16 +      SOME t' => t'
    1.17 +    | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";
    1.18  
    1.19  val SOME (t,_) = rewrite_inst_ thy e_rew_ord e_rls true subst 
    1.20    (num_str @{thm "int_isolate_add"}) t; term2str t;
    1.21 @@ -63,7 +70,9 @@
    1.22  val thy = @{theory "Test"};
    1.23  "----------- rewriting for usecase2 ---------------------";
    1.24  
    1.25 -val t = parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)";
    1.26 +val t = case parseNEW ctxt "xxx + abc + -1 * 111 + (123::int)" of
    1.27 +      SOME t' => t'
    1.28 +    | NONE => error "diophanteq.sml: syntax error in rewriting for usecase2";
    1.29  
    1.30  val SOME (thmID,thm) = get_calculation_ thy (the(assoc(calclist,"TIMES"))) t; 
    1.31  val SOME (t,_) = rewrite_ thy tless_true tval_rls true thm t; term2str t;