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)