# HG changeset patch
# User Walther Neuper <neuper@ist.tugraz.at>
# Date 1285943373 -7200
# Node ID d164e328db740b1d2a8d900df459d2e9a27cd1da
# Parent  a51a7033419189655112836ea01884dd77156f5e
tuned: tests go through

diff -r a51a70334191 -r d164e328db74 test/Tools/isac/Knowledge/polyminus.sml
--- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 01 16:23:03 2010 +0200
+++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 01 16:29:33 2010 +0200
@@ -599,43 +599,9 @@
 	                "     matchsub (?a + (?b - ?c)) t_t | " ^
 	                "     matchsub (?a - (?b + ?c)) t_t | " ^
 	                "     matchsub (?a + (?b - ?c)) t_t )");
+show_types := true;
 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)"
-then () else error "polyminus.sml type-structure of \"?a :: real\" changed";
-show_types := false;
-
-"===== deconstruct datatype typ ===";
-val str = "?a";
-val t = (thy, str) |>> thy2ctxt 
-                   |-> ProofContext.read_term_pattern
-                   |> numbers_to_string;
-val Var (("a", 0), ty) = t;
-val TVar ((str, i), srt) = ty;
-if str = "'a" andalso i = 1 andalso srt = [] then ()
-else error "termC.sml type-structure of \"?a\" changed";
-
-"----- real type in pattern ---";
-val str = "?a :: real";
-val t = (thy, str) |>> thy2ctxt 
-                   |-> ProofContext.read_term_pattern
-                   |> numbers_to_string;
-val Var (("a", 0), ty) = t;
-val Type (str, tys) = ty;
-if str = "RealDef.real" andalso tys = [] andalso ty = HOLogic.realT then ()
-else error "termC.sml type-structure of \"?a :: real\" changed";
-
-"===== Not (matchsub (?a + (?b + ?c)) t_t |... ===";
-val (thy, str) = (thy, "Not (matchsub (?a + (?b + ?c)) t_t | " ^
-	               "     matchsub (?a + (?b - ?c)) t_t | " ^
-	               "     matchsub (?a - (?b + ?c)) t_t | " ^
-	               "     matchsub (?a + (?b - ?c)) t_t )");
-"----- read_term_pattern ---";
-val t = (thy, str) |>> thy2ctxt 
-                   |-> ProofContext.read_term_pattern
-                   |> numbers_to_string;
-show_types := true;
-val t1 = typ_a2real t;
-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)"
-then () else error "termC.sml type-structure of \"?a :: real\" changed expl";
+then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
 show_types := false;
 
 (*========== inhibit exn =======================================================