1.1 --- a/test/Tools/isac/IsacKnowledge/rooteq.sml	Wed Aug 18 13:53:15 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/rooteq.sml	Wed Aug 18 13:55:23 2010 +0200
     1.3 @@ -16,62 +16,62 @@
     1.4  "--------------(sqrt(x+1)+sqrt(4*x+4)=sqrt(9*x+9))-----------------";
     1.5  
     1.6  val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
     1.7 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
     1.8 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
     1.9  val result = term2str t_;
    1.10  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.11  
    1.12  val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_rootTerm_in  x";
    1.13 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.14 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.15  val result = term2str t_;
    1.16  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.17  
    1.18  val t = (term_of o the o (parse RootEq.thy)) "(nroot 5 (x+4)) is_rootTerm_in  x";
    1.19 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.20 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.21  val result = term2str t_;
    1.22  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.23  
    1.24  val t = (term_of o the o (parse RootEq.thy)) "(sqrt(2+x+3)) is_sqrtTerm_in  x";
    1.25 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.26 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.27  val result = term2str t_;
    1.28  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.29  
    1.30  val t = (term_of o the o (parse RootEq.thy)) "(sqrt(25)) is_sqrtTerm_in  x";
    1.31 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.32 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.33  val result = term2str t_;
    1.34  if result <>  "False"  then raise error "rooteq.sml: new behaviour:" else ();
    1.35  
    1.36  val t = (term_of o the o (parse RootEq.thy)) "sqrt(1 + x) is_normSqrtTerm_in x";
    1.37 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.38 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.39  val result = term2str t_;
    1.40  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.41  
    1.42  val t = (term_of o the o (parse RootEq.thy)) "(3+3*sqrt(x)) is_normSqrtTerm_in x";
    1.43 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.44 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.45  val result = term2str t_;
    1.46  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.47  
    1.48  val t = (term_of o the o (parse RootEq.thy)) "(sqrt(x+1)+1) is_normSqrtTerm_in x";
    1.49 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.50 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.51  val result = term2str t_;
    1.52  if result <>  "False"  then raise error "rooteq.sml: new behaviour:" else ();
    1.53  
    1.54  val t = (term_of o the o (parse RootEq.thy)) "(1 - u/(sqrt(r - u))) is_normSqrtTerm_in u";
    1.55 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.56 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.57  val result = term2str t_;
    1.58  if result <>  "False"  then raise error "rooteq.sml: new behaviour:" else ();
    1.59  
    1.60  val t = (term_of o the o (parse RootEq.thy)) "(x*(1+x)/(sqrt(x+1))) is_normSqrtTerm_in x";
    1.61 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.62 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.63  val result = term2str t_;
    1.64  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.65  
    1.66  val t = (term_of o the o (parse RootEq.thy)) "(1 - (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in  x";
    1.67 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.68 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.69  val result = term2str t_;
    1.70  if result <>  "False"  then raise error "rooteq.sml: new behaviour:" else ();
    1.71  
    1.72  val t = (term_of o the o (parse RootEq.thy)) "(1 + (sqrt(2+x+3)^^^3)) is_normSqrtTerm_in  x";
    1.73 -val Some(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.74 +val SOME(t_, _) = rewrite_set_ RootEq.thy  false RootEq_prls t;
    1.75  val result = term2str t_;
    1.76  if result <>  "True"  then raise error "rooteq.sml: new behaviour:" else ();
    1.77