# HG changeset patch
# User haftmann
# Date 1245253366 -7200
# Node ID 9fc407df200ca2d0ee04c55850edcaf64443aab0
# Parent  fd841fc9ee9ed5f49a252a740c32cbd5d15d98fc
uncheck is liberal wrt. semityped terms

diff -r fd841fc9ee9e -r 9fc407df200c src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Wed Jun 17 17:42:41 2009 +0200
+++ b/src/Pure/Isar/overloading.ML	Wed Jun 17 17:42:46 2009 +0200
@@ -91,12 +91,17 @@
       |> mark_passed)
   end;
 
+fun rewrite_liberal thy unchecks t =
+  case try (Pattern.rewrite_term thy unchecks []) t
+   of NONE => NONE
+    | SOME t' => if t aconv t' then NONE else SOME t';
+
 fun improve_term_uncheck ts ctxt =
   let
     val thy = ProofContext.theory_of ctxt;
     val unchecks = (#unchecks o ImprovableSyntax.get) ctxt;
-    val ts' = map (Pattern.rewrite_term thy unchecks []) ts;
-  in if eq_list (op aconv) (ts, ts') then NONE else SOME (ts', ctxt) end;
+    val ts' = map (rewrite_liberal thy unchecks) ts;
+  in if exists is_some ts' then SOME (map2 the_default ts ts', ctxt) else NONE end;
 
 fun set_primary_constraints ctxt =
   let