1.1 --- a/src/Tools/isac/Interpret/calchead.sml	Sat Feb 26 12:53:00 2011 +0100
     1.2 +++ b/src/Tools/isac/Interpret/calchead.sml	Tue Mar 01 15:23:59 2011 +0100
     1.3 @@ -711,7 +711,7 @@
     1.4  
     1.5  fun test_types thy (d,ts) =
     1.6    let 
     1.7 -    val s = !show_types; val _ = show_types:= true;
     1.8 +    (*val s = !show_types; val _ = show_types:= true;*)
     1.9      val opt = (try (comp_dts thy)) (d,ts);
    1.10      val msg = case opt of 
    1.11        SOME _ => "" 
    1.12 @@ -720,7 +720,7 @@
    1.13  	       ((strs2str' o map (Print_Mode.setmp [] (Syntax.string_of_term
    1.14                                                             (thy2ctxt thy)))) ts)
    1.15  	     ^ " is illtyped");
    1.16 -    val _ = show_types:= s
    1.17 +    (*val _ = show_types:= s*)
    1.18    in msg end;
    1.19  
    1.20  
    1.21 @@ -887,7 +887,9 @@
    1.22  	^"*** typeconstructor in script: "^(term_detail2str ty)
    1.23  	^"*** checked by theory: "^(theory2str thy)^"\n"
    1.24  	^"*** " ^ dots 66);
    1.25 -	    OldGoals.print_exn e; (*raises exn again*)
    1.26 +	    (*OldGoals.print_exn e; raises exn again*)
    1.27 +            writeln (PolyML.makestring e);
    1.28 +            reraise e;
    1.29  	(*raise ERROR "actual args do not match formal args";FIXXXME.WN100916*)
    1.30  	NONE);
    1.31  
    1.32 @@ -961,8 +963,8 @@
    1.33  
    1.34  (*.report part of the error-msg which is not available in match_args.*)
    1.35  fun match_ags_msg pI stac ags =
    1.36 -    let val s = !show_types
    1.37 -	val _ = show_types:= true
    1.38 +    let (*val s = !show_types
    1.39 +	val _ = show_types:= true*)
    1.40  	val pats = (#ppc o get_pbt) pI
    1.41  	val msg = (dots 70^"\n"
    1.42  		 ^"*** problem "^strs2str pI^" has the ...\n"
    1.43 @@ -971,7 +973,7 @@
    1.44  		 ^"*** arg-list "^terms2str ags^"\n"
    1.45  		 ^dashs 70)
    1.46  	(*WN100921 ^^^^ expect TYPE errormsg below; lost with Isa09*)
    1.47 -	val _ = show_types:= s
    1.48 +	(*val _ = show_types:= s*)
    1.49      in tracing msg end;
    1.50  
    1.51