1.1 --- a/src/HOL/Tools/meson.ML	Wed Jun 20 17:32:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Jun 20 17:34:44 2007 +0200
     1.3 @@ -77,13 +77,24 @@
     1.4  fun first_order_resolve thA thB =
     1.5    let val thy = theory_of_thm thA
     1.6        val tmA = concl_of thA
     1.7 -      fun match pat = Pattern.first_order_match thy (pat,tmA) (tyenv0,tenv0)
     1.8        val Const("==>",_) $ tmB $ _ = prop_of thB
     1.9 -      val (tyenv,tenv) = match tmB
    1.10 +      val (tyenv,tenv) = Pattern.first_order_match thy (tmB,tmA) (tyenv0,tenv0)
    1.11        val ct_pairs = map (pairself (cterm_of thy) o term_pair_of) (Vartab.dest tenv)
    1.12    in  thA RS (cterm_instantiate ct_pairs thB)  end
    1.13    handle _ => raise THM ("first_order_resolve", 0, [thA,thB]);
    1.14  
    1.15 +fun flexflex_first_order th = 
    1.16 +  case (tpairs_of th) of
    1.17 +      [] => th
    1.18 +    | pairs =>
    1.19 +	let val thy = theory_of_thm th
    1.20 +	    val (tyenv,tenv) = 
    1.21 +	          foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
    1.22 +	    val t_pairs = map term_pair_of (Vartab.dest tenv)
    1.23 +	    val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
    1.24 +	in  th'  end
    1.25 +	handle THM _ => th;
    1.26 +
    1.27  (*raises exception if no rules apply -- unlike RL*)
    1.28  fun tryres (th, rls) = 
    1.29    let fun tryall [] = raise THM("tryres", 0, th::rls)