Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/thm.ML
changeset 13642 a3d97348ceb6
parent 13629 a46362d2b19b
child 13658 c9ad3e64ddcf 
--- a/src/Pure/thm.ML	Thu Oct 10 14:26:50 2002 +0200
+++ b/src/Pure/thm.ML	Thu Oct 10 19:02:23 2002 +0200
@@ -1386,7 +1386,8 @@
         val comp = bicompose_aux match (state, (stpairs, Bs, Bi, C), true);
         fun res [] = Seq.empty
           | res ((eres_flg, rule)::brules) =
-              if could_bires (Hs, B, eres_flg, rule)
+              if !Pattern.trace_unify_fail orelse
+                 could_bires (Hs, B, eres_flg, rule)
               then Seq.make (*delay processing remainder till needed*)
                   (fn()=> Some(comp (eres_flg, lift rule, nprems_of rule),
                                res brules))
isabelle