# HG changeset patch
# User blanchet
# Date 1285866947 -7200
# Node ID a91a84b1dfdd49e622247a6484da66e50a9ada0e
# Parent  35ae5cf8c96a5ef0c6242ccf1755109bc18f0beb
reintroduced code that keeps track of whether the Isabelle and Metis proofs are in sync -- generalized to work with the new skolemizer

diff -r 35ae5cf8c96a -r a91a84b1dfdd src/HOL/Tools/Sledgehammer/metis_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 18:59:37 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_reconstruct.ML	Thu Sep 30 19:15:47 2010 +0200
@@ -528,6 +528,12 @@
         in  th'  end
         handle THM _ => th;
 
+fun is_metis_literal_genuine (_, (s, _)) = not (String.isPrefix class_prefix s)
+fun is_isabelle_literal_genuine t =
+  case t of _ $ (Const (@{const_name skolem}, _) $ _) => false | _ => true
+
+fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
+
 fun replay_one_inference ctxt mode old_skolems (fol_th, inf) thpairs =
   let
     val _ = trace_msg (fn () => "=============================================")
@@ -537,6 +543,13 @@
              |> flexflex_first_order
     val _ = trace_msg (fn () => "ISABELLE THM: " ^ Display.string_of_thm ctxt th)
     val _ = trace_msg (fn () => "=============================================")
+    val num_metis_lits =
+      fol_th |> Metis_Thm.clause |> Metis_LiteralSet.toList
+             |> count is_metis_literal_genuine
+    val num_isabelle_lits =
+      th |> prems_of |> count is_isabelle_literal_genuine
+    val _ = if num_metis_lits = num_isabelle_lits then ()
+            else error "Cannot replay Metis proof in Isabelle: Out of sync."
   in (fol_th, th) :: thpairs end
 
 end;