1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 01 16:23:03 2010 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 01 16:29:33 2010 +0200
     1.3 @@ -599,43 +599,9 @@
     1.4  	                "     matchsub (?a + (?b - ?c)) t_t | " ^
     1.5  	                "     matchsub (?a - (?b + ?c)) t_t | " ^
     1.6  	                "     matchsub (?a + (?b - ?c)) t_t )");
     1.7 +show_types := true;
     1.8  if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c)) t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
     1.9 -then () else error "polyminus.sml type-structure of \"?a :: real\" changed";
    1.10 -show_types := false;
    1.11 -
    1.12 -"===== deconstruct datatype typ ===";
    1.13 -val str = "?a";
    1.14 -val t = (thy, str) |>> thy2ctxt 
    1.15 -                   |-> ProofContext.read_term_pattern
    1.16 -                   |> numbers_to_string;
    1.17 -val Var (("a", 0), ty) = t;
    1.18 -val TVar ((str, i), srt) = ty;
    1.19 -if str = "'a" andalso i = 1 andalso srt = [] then ()
    1.20 -else error "termC.sml type-structure of \"?a\" changed";
    1.21 -
    1.22 -"----- real type in pattern ---";
    1.23 -val str = "?a :: real";
    1.24 -val t = (thy, str) |>> thy2ctxt 
    1.25 -                   |-> ProofContext.read_term_pattern
    1.26 -                   |> numbers_to_string;
    1.27 -val Var (("a", 0), ty) = t;
    1.28 -val Type (str, tys) = ty;
    1.29 -if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT then ()
    1.30 -else error "termC.sml type-structure of \"?a :: real\" changed";
    1.31 -
    1.32 -"===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";
    1.33 -val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^
    1.34 -	               "     matchsub (?a + (?b - ?c)) t_t | " ^
    1.35 -	               "     matchsub (?a - (?b + ?c)) t_t | " ^
    1.36 -	               "     matchsub (?a + (?b - ?c)) t_t )");
    1.37 -"----- read_term_pattern ---";
    1.38 -val t = (thy, str) |>> thy2ctxt 
    1.39 -                   |-> ProofContext.read_term_pattern
    1.40 -                   |> numbers_to_string;
    1.41 -show_types := true;
    1.42 -val t1 = typ_a2real t;
    1.43 -if term2str t1 = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c)) t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
    1.44 -then () else error "termC.sml type-structure of \"?a :: real\" changed expl";
    1.45 +then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
    1.46  show_types := false;
    1.47  
    1.48  (*========== inhibit exn =======================================================