# HG changeset patch
# User paulson
# Date 1132151363 -3600
# Node ID 7858b777569ae1bd623fbdd22634ccbbfc02da62
# Parent  c6e3c6516a239e864cdf7a69547b1c308593b1b7
new version of "tryres" allowing multiple unifiers (apparently needed for
Skolemization of higher-order theorems)

diff -r c6e3c6516a23 -r 7858b777569a src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Nov 16 14:05:41 2005 +0100
+++ b/src/HOL/Tools/meson.ML	Wed Nov 16 15:29:23 2005 +0100
@@ -65,10 +65,13 @@
 
 (**** Operators for forward proof ****)
 
+(*Like RS, but raises Option if there are no unifiers and allows multiple unifiers.*)
+fun resolve1 (tha,thb) = Seq.hd (biresolution false [(false,tha)] 1 thb);
+
 (*raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rls) = 
   let fun tryall [] = raise THM("tryres", 0, th::rls)
-        | tryall (rl::rls) = (th RS rl handle THM _ => tryall rls)
+        | tryall (rl::rls) = (resolve1(th,rl) handle Option => tryall rls)
   in  tryall rls  end;
   
 (*Permits forward proof from rules that discharge assumptions*)