# HG changeset patch
# User paulson
# Date 1223482176 -7200
# Node ID 0cf2749e8ef730dbcebe424485424a4b8ff9a534
# Parent  82b36daff4c13144e1a54473ca046cc5ec7a7a8c
The result of the equality inference rule no longer undergoes factoring.

diff -r 82b36daff4c1 -r 0cf2749e8ef7 src/HOL/Tools/metis_tools.ML
--- a/src/HOL/Tools/metis_tools.ML	Wed Oct 08 00:25:38 2008 +0200
+++ b/src/HOL/Tools/metis_tools.ML	Wed Oct 08 18:09:36 2008 +0200
@@ -327,7 +327,9 @@
         val _ = app (fn (x,y) => Output.debug (fn () => Display.string_of_cterm x ^ " |-> " ^
                                                         Display.string_of_cterm y))
                   substs'
-    in  cterm_instantiate substs' i_th  end;
+    in  cterm_instantiate substs' i_th  
+        handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
+    end;
 
   (* INFERENCE RULE: RESOLVE *)
 
@@ -430,21 +432,21 @@
                            (ListPair.zip (term_vars (prop_of subst'), [tm_abs, tm_subst, i_tm]))
     in  cterm_instantiate eq_terms subst'  end;
 
+  val factor = Seq.hd o distinct_subgoals_tac;
+
   fun step ctxt isFO thpairs (fol_th, Metis.Proof.Axiom _)                        =
-        axiom_inf ctxt thpairs fol_th
+        factor (axiom_inf ctxt thpairs fol_th)
     | step ctxt isFO thpairs (_, Metis.Proof.Assume f_atm)                        =
         assume_inf ctxt f_atm
-    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))                =
-        inst_inf ctxt thpairs f_subst f_th1
+    | step ctxt isFO thpairs (_, Metis.Proof.Subst(f_subst, f_th1))               =
+        factor (inst_inf ctxt thpairs f_subst f_th1)
     | step ctxt isFO thpairs (_, Metis.Proof.Resolve(f_atm, f_th1, f_th2))        =
-        resolve_inf ctxt thpairs f_atm f_th1 f_th2
+        factor (resolve_inf ctxt thpairs f_atm f_th1 f_th2)
     | step ctxt isFO thpairs (_, Metis.Proof.Refl f_tm)                           =
         refl_inf ctxt f_tm
     | step ctxt isFO thpairs (_, Metis.Proof.Equality(f_lit, f_p, f_r)) =
         equality_inf ctxt isFO thpairs f_lit f_p f_r;
 
-  val factor = Seq.hd o distinct_subgoals_tac;
-
   fun real_literal (b, (c, _)) = not (String.isPrefix ResClause.class_prefix c);
 
   fun translate isFO _    thpairs [] = thpairs
@@ -452,7 +454,7 @@
         let val _ = Output.debug (fn () => "=============================================")
             val _ = Output.debug (fn () => "METIS THM: " ^ Metis.Thm.toString fol_th)
             val _ = Output.debug (fn () => "INFERENCE: " ^ Metis.Proof.inferenceToString inf)
-            val th = Meson.flexflex_first_order (factor (step ctxt isFO thpairs (fol_th, inf)))
+            val th = Meson.flexflex_first_order (step ctxt isFO thpairs (fol_th, inf))
             val _ = Output.debug (fn () => "ISABELLE THM: " ^ Display.string_of_thm th)
             val _ = Output.debug (fn () => "=============================================")
             val n_metis_lits = length (filter real_literal (Metis.LiteralSet.toList (Metis.Thm.clause fol_th)))