# HG changeset patch
# User haftmann
# Date 1207781200 -7200
# Node ID ff250dde68d657a74a7bd9eaac5646babb898ca9
# Parent  07d7d0a6d5fd2af318c1cc85bb3438a557661424
improvements are strict

diff -r 07d7d0a6d5fd -r ff250dde68d6 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Thu Apr 10 00:46:38 2008 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Apr 10 00:46:40 2008 +0200
@@ -66,7 +66,7 @@
       ImprovableSyntax.get ctxt;
     val tsig = (Sign.tsig_of o ProofContext.theory_of) ctxt;
     fun accumulate_improvements (Const (c, ty)) = (case improve (c, ty)
-         of SOME ty_ty' => (perhaps o try o Type.typ_match tsig) ty_ty'
+         of SOME ty_ty' => Type.typ_match tsig ty_ty'
           | _ => I)
       | accumulate_improvements _ = I;
     val improvements = (fold o fold_aterms) accumulate_improvements ts Vartab.empty;