merged

--- a/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 14:10:57 2013 +0100
+++ b/src/HOL/Metis_Examples/Clausification.thy	Thu Jan 03 14:12:12 2013 +0100
@@ -10,10 +10,6 @@
 imports Complex_Main
 begin
 
-(* FIXME: shouldn't need this *)
-declare [[unify_search_bound = 100]]
-declare [[unify_trace_bound = 100]]
-
 
 text {* Definitional CNF for facts *}
 
@@ -139,7 +135,7 @@
 lemma
   "(\<exists>x \<in> set xs. P x) \<longleftrightarrow>
    (\<exists>ys x zs. xs = ys @ x # zs \<and> P x \<and> (\<forall>z \<in> set zs. \<not> P z))"
-by (metis split_list_last_prop [where P = P] in_set_conv_decomp)
+by (metis split_list_last_prop[where P = P] in_set_conv_decomp)
 
 lemma ex_tl: "EX ys. tl ys = xs"
 using tl.simps(2) by fast

--- a/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:10:57 2013 +0100
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Jan 03 14:12:12 2013 +0100
@@ -167,21 +167,36 @@
           (rename_bound_vars_RS th rl handle THM _ => tryall rls)
   in  tryall rls  end;
 
+(* Special version of "rtac" that works around an explosion in the unifier.
+   If the goal has the form "?P c", the danger is that unifying "?P" with a
+   formula of the form "... c ... c ... c ..." will lead to a huge unification
+   problem, due to the (spurious) choices between projection and imitation. The
+   workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
+fun quant_rtac th i st =
+  case (concl_of st, prop_of th) of
+    (@{const Trueprop} $ (Var _ $ (c as Free _)), @{const Trueprop} $ _) =>
+    let
+      val cc = cterm_of (theory_of_thm th) c
+      val ct = Thm.dest_arg (cprop_of th)
+    in rtac th i (Drule.instantiate' [] [SOME (Thm.lambda cc ct)] st) end
+  | _ => rtac th i st
+
 (*Permits forward proof from rules that discharge assumptions. The supplied proof state st,
   e.g. from conj_forward, should have the form
     "[| P' ==> ?P; Q' ==> ?Q |] ==> ?P & ?Q"
   and the effect should be to instantiate ?P and ?Q with normalized versions of P' and Q'.*)
 fun forward_res ctxt nf st =
-  let fun forward_tacf [prem] = rtac (nf prem) 1
-        | forward_tacf prems =
-            error (cat_lines
-              ("Bad proof state in forward_res, please inform [e-mail]:" ::
-                Display.string_of_thm ctxt st ::
-                "Premises:" :: map (Display.string_of_thm ctxt) prems))
+  let
+    fun tacf [prem] = quant_rtac (nf prem) 1
+      | tacf prems =
+        error (cat_lines
+          ("Bad proof state in forward_res, please inform [e-mail]:" ::
+            Display.string_of_thm ctxt st ::
+            "Premises:" :: map (Display.string_of_thm ctxt) prems))
   in
-    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS forward_tacf) st)
-    of SOME(th,_) => th
-     | NONE => raise THM("forward_res", 0, [st])
+    case Seq.pull (ALLGOALS (Misc_Legacy.METAHYPS tacf) st) of
+      SOME (th, _) => th
+    | NONE => raise THM ("forward_res", 0, [st])
   end;
 
 (*Are any of the logical connectives in "bs" present in the term?*)
@@ -635,7 +650,6 @@
 
 val abs_extensionalize_thm = Conv.fconv_rule o abs_extensionalize_conv
 
-(* "RS" can fail if "unify_search_bound" is too small. *)
 fun try_skolemize_etc ctxt th =
   let
     val thy = Proof_Context.theory_of ctxt