# HG changeset patch
# User blanchet
# Date 1288084283 -7200
# Node ID a88d6073b190197f4737f8a0d7cb8f51e2756a23
# Parent  a2f01956220e8fb1dd4345fd974548329ca3b5da
clearer error messages

diff -r a2f01956220e -r a88d6073b190 src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 26 11:10:00 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Oct 26 11:11:23 2010 +0200
@@ -754,8 +754,8 @@
         |> fold Int_Pair_Graph.add_deps_acyclic depss
         |> Int_Pair_Graph.topological_order
         handle Int_Pair_Graph.CYCLES _ =>
-               error "Cannot replay Metis proof in Isabelle without axiom of \
-                     \choice."
+               error "Cannot replay Metis proof in Isabelle without \
+                     \\"Hilbert_Choice\"."
       val params0 =
         [] |> fold (Term.add_vars o snd) (map_filter I axioms)
            |> map (`(Meson_Clausify.cluster_of_zapped_var_name o fst o fst))
@@ -796,6 +796,9 @@
                        THEN rotate_tac (rotation_for_subgoal i) i
 (*                       THEN PRIMITIVE (unify_first_prem_with_concl thy i) ###*)
                        THEN assume_tac i)))
+      handle ERROR _ =>
+             error ("Cannot replay Metis proof in Isabelle:\n\
+                    \Error when discharging Skolem assumptions.")
     end
 
 val setup = trace_setup