test/Tools/isac/Knowledge/diophanteq.sml
branchdecompose-isar
changeset 41951 50bc995aa45b
parent 41949 c1859b72ae8d
child 42166 911c49949ba9
     1.1 --- a/test/Tools/isac/Knowledge/diophanteq.sml	Wed Apr 06 18:01:02 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/diophanteq.sml	Thu Apr 07 16:31:05 2011 +0200
     1.3 @@ -26,12 +26,9 @@
     1.4  "----------- rewriting for usecase1 ---------------------";
     1.5  "----------- rewriting for usecase1 ---------------------";
     1.6  "----------- rewriting for usecase1 ---------------------";
     1.7 -val subst = let
     1.8 -      val pair = (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int");
     1.9 -    in case pair of
    1.10 -        (SOME r, SOME s) => [(r,s)]
    1.11 -      | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
    1.12 -    end;
    1.13 +val subst = case (parseNEW ctxt "bdv::int", parseNEW ctxt "xxx::int") of
    1.14 +      (SOME r, SOME s) => [(r,s)]
    1.15 +    | _ => error "diophanteq.sml: syntax error in rewriting for usecase1"
    1.16  val t = case parseNEW ctxt "xxx + 111 = abc + (123::int)" of
    1.17        SOME t' => t'
    1.18      | NONE => error "diophanteq.sml: syntax error in rewriting for usecase1";