# HG changeset patch
# User blanchet
# Date 1286202980 -7200
# Node ID 8f415cfc2180a940e423f3e536c61c2c253baa72
# Parent  56409c11195dd062c4f331e3fdd166cbd33fd0bc
put two operations in the right order

diff -r 56409c11195d -r 8f415cfc2180 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Oct 04 16:24:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Mon Oct 04 16:36:20 2010 +0200
@@ -204,7 +204,7 @@
       val thy = ProofContext.theory_of ctxt
       (* distinguish variables with same name but different types *)
       val prems_imp_false' =
-        prems_imp_false |> try (forall_intr_vars o gen_all)
+        prems_imp_false |> try (forall_intr_vars #> gen_all)
                         |> the_default prems_imp_false
       val prems_imp_false =
         if prop_of prems_imp_false aconv prop_of prems_imp_false' then
@@ -284,7 +284,8 @@
         "; tysubst: " ^ PolyML.makestring tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
                      o pairself (Syntax.string_of_term ctxt)) tsubst) ^ "}"
-      val _ = tracing ("SUBSTS:\n" ^ cat_lines (map string_for_subst_info substs))
+      val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
+                       cat_lines (map string_for_subst_info substs))
       val _ = tracing ("OUTERMOST SKOLEMS: " ^ PolyML.makestring params0)
       val _ = tracing ("ORDERED CLUSTERS: " ^ PolyML.makestring ordered_clusters)
       val _ = tracing ("AXIOM COUNTS: " ^ PolyML.makestring ax_counts)