fixed warning;
authorwenzelm
Thu Nov 27 19:36:31 1997 +0100 (1997-11-27)
changeset 4314a6eb21e10090
parent 4313 03353197410c
child 4315 f4bc2f6ee5e0
fixed warning;
src/Pure/unify.ML
     1.1 --- a/src/Pure/unify.ML	Thu Nov 27 19:36:08 1997 +0100
     1.2 +++ b/src/Pure/unify.ML	Thu Nov 27 19:36:31 1997 +0100
     1.3 @@ -631,7 +631,7 @@
     1.4  	      [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq)
     1.5  	    | dp::frigid' => 
     1.6  		if tdepth > !search_bound then
     1.7 -		    (prs"***Unification bound exceeded\n"; Seq.pull reseq)
     1.8 +		    (warning "Unification bound exceeded"; Seq.pull reseq)
     1.9  		else
    1.10  		(if tdepth > !trace_bound then
    1.11  		    print_dpairs "Enter MATCH" (env',flexrigid@flexflex)