author | wenzelm |
Thu, 27 Nov 1997 19:36:31 +0100 | |
changeset 4314 | a6eb21e10090 |
parent 4313 | 03353197410c |
child 4315 | f4bc2f6ee5e0 |
src/Pure/unify.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/unify.ML Thu Nov 27 19:36:08 1997 +0100 +++ b/src/Pure/unify.ML Thu Nov 27 19:36:31 1997 +0100 @@ -631,7 +631,7 @@ [] => Some (foldr add_ffpair (flexflex, (env',[])), reseq) | dp::frigid' => if tdepth > !search_bound then - (prs"***Unification bound exceeded\n"; Seq.pull reseq) + (warning "Unification bound exceeded"; Seq.pull reseq) else (if tdepth > !trace_bound then print_dpairs "Enter MATCH" (env',flexrigid@flexflex)