src/HOL/Import/shuffler.ML
changeset 15661 9ef583b08647
parent 15574 b1d1b5bfc464
child 15794 5de27a5fc5ed
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Apr 07 09:24:35 2005 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Apr 07 09:25:33 2005 +0200
     1.3 @@ -304,7 +304,7 @@
     1.4  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
     1.5  	    in
     1.6  		if not (lhs aconv origt)
     1.7 -		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
     1.8 +		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
     1.9  		      writeln (string_of_cterm (cterm_of sg origt));
    1.10  		      writeln (string_of_cterm (cterm_of sg lhs));
    1.11  		      writeln (string_of_cterm (cterm_of sg typet));
    1.12 @@ -359,7 +359,7 @@
    1.13  		val lhs = #1 (Logic.dest_equals (prop_of (final init)))
    1.14  	    in
    1.15  		if not (lhs aconv origt)
    1.16 -		then (writeln "SOMEthing is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.17 +		then (writeln "Something is utterly wrong: (orig,lhs,frozen type,t,tinst)";
    1.18  		      writeln (string_of_cterm (cterm_of sg origt));
    1.19  		      writeln (string_of_cterm (cterm_of sg lhs));
    1.20  		      writeln (string_of_cterm (cterm_of sg typet));