1.1 --- a/test/Tools/isac/IsacKnowledge/atools.sml	Tue Aug 17 09:05:51 2010 +0200
     1.2 +++ b/test/Tools/isac/IsacKnowledge/atools.sml	Wed Aug 18 13:40:09 2010 +0200
     1.3 @@ -23,9 +23,9 @@
     1.4  "----------- occurs_in -------------------------------------------";
     1.5  "----------- occurs_in -------------------------------------------";
     1.6  "----------- occurs_in -------------------------------------------";
     1.7 -fun str2t str = (term_of o the o (parse thy )) str;
     1.8 +fun str2term str = (term_of o the o (parse thy )) str;
     1.9  fun term2s t = Sign.string_of_term (sign_of thy) t;
    1.10 -val t = str2t "x";
    1.11 +val t = str2term "x";
    1.12  if occurs_in t t then "OK" else raise error "atools.sml: occurs_in x x -> f";
    1.13  
    1.14  val t = str2term "x occurs_in x";
    1.15 @@ -53,7 +53,7 @@
    1.16  "----------- argument_of -----------------------------------------";
    1.17  "----------- argument_of -----------------------------------------";
    1.18  "----------- argument_of -----------------------------------------";
    1.19 -val t = str2t "argument_in (M_b x)";
    1.20 +val t = str2term "argument_in (M_b x)";
    1.21  val Some (str, t') = eval_argument_in 0 "Atools.argument'_in" t 0;
    1.22  if term2s t' = "(argument_in M_b x) = x" then ()
    1.23  else raise error "atools.sml:(argument_in M_b x) = x  ???";