# HG changeset patch
# User paulson
# Date 1182353684 -7200
# Node ID 37860871f241a0d8848964b48b89d0c64bc08e0a
# Parent  8c7da8649f2f5e8dd056a260f41cae5493fea8dc
Added flexflex_first_order and tidied first_order_resolution

diff -r 8c7da8649f2f -r 37860871f241 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Jun 20 17:32:53 2007 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Jun 20 17:34:44 2007 +0200
@@ -77,13 +77,24 @@
 fun first_order_resolve thA thB =
   let val thy = theory_of_thm thA
       val tmA = concl_of thA
-      fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
       val Const("==>",_) $ tmB $ _ = prop_of thB
-      val (tyenv,tenv) = match tmB
+      val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
       val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
   in  thA RS (cterm_instantiate ct_pairs thB)  end
   handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
 
+fun flexflex_first_order th = 
+  case (tpairs_of th) of
+      [] => th
+    | pairs =>
+	let val thy = theory_of_thm th
+	    val (tyenv,tenv) = 
+	          foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
+	    val t_pairs = map term_pair_of (Vartab.dest tenv)
+	    val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
+	in  th'  end
+	handle THM _ => th;
+
 (*raises exception if no rules apply -- unlike RL*)
 fun tryres (th, rls) = 
   let fun tryall [] = raise THM("tryres", 0, th::rls)