diff -r 0a36a8722b80 -r b772eb34c16c src/Tools/isac/Interpret/calchead.sml
--- a/src/Tools/isac/Interpret/calchead.sml	Sat Feb 26 12:53:00 2011 +0100
+++ b/src/Tools/isac/Interpret/calchead.sml	Tue Mar 01 15:23:59 2011 +0100
@@ -711,7 +711,7 @@
 
 fun test_types thy (d,ts) =
   let 
-    val s = !show_types; val _ = show_types:= true;
+    (*val s = !show_types; val _ = show_types:= true;*)
     val opt = (try (comp_dts thy)) (d,ts);
     val msg = case opt of 
       SOME _ => "" 
@@ -720,7 +720,7 @@
 	       ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
                                                            (thy2ctxt thy)))) ts)
 	     ^ " is illtyped");
-    val _ = show_types:= s
+    (*val _ = show_types:= s*)
   in msg end;
 
 
@@ -887,7 +887,9 @@
 	^"*** typeconstructor in script: "^(term_detail2str ty)
 	^"*** checked by theory: "^(theory2str thy)^"\n"
 	^"*** " ^ dots 66);
-	    OldGoals.print_exn e; (*raises exn again*)
+	    (*OldGoals.print_exn e; raises exn again*)
+            writeln (PolyML.makestring e);
+            reraise e;
 	(*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
 	NONE);
 
@@ -961,8 +963,8 @@
 
 (*.report part of the error-msg which is not available in match_args.*)
 fun match_ags_msg pI stac ags =
-    let val s = !show_types
-	val _ = show_types:= true
+    let (*val s = !show_types
+	val _ = show_types:= true*)
 	val pats = (#ppc o get_pbt) pI
 	val msg = (dots 70^"\n"
 		 ^"*** problem "^strs2str pI^" has the ...\n"
@@ -971,7 +973,7 @@
 		 ^"*** arg-list "^terms2str ags^"\n"
 		 ^dashs 70)
 	(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
-	val _ = show_types:= s
+	(*val _ = show_types:= s*)
     in tracing msg end;