# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID b98daa96d04352dcc4047a87e723012395a3bb53
# Parent  ea57961db57ef447acdae4a9ae6a4464bd93d541
don't pass "~ " to new Metis

diff -r ea57961db57e -r b98daa96d043 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -318,25 +318,29 @@
     uncurry (union (op =)) (pairself metis_literals_from_atp (phi1, phi2))
   | metis_literals_from_atp phi = [metis_literal_from_atp phi]
 fun metis_axiom_from_atp clauses (Formula (ident, _, phi, _, _)) =
-    (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
-         |> Metis_Thm.axiom,
-     if ident = type_tag_idempotence_helper_name orelse
-        String.isPrefix lightweight_tags_sym_formula_prefix ident then
-       Isa_Reflexive_or_Trivial
-     else if String.isPrefix helper_prefix ident then
-       case space_explode "_" ident  of
-         _ :: const :: j :: _ =>
-         Isa_Raw (nth (AList.lookup (op =) helper_table const |> the |> snd)
-                      (the (Int.fromString j) - 1)
-                  |> prepare_helper)
-       | _ => raise Fail ("malformed helper identifier " ^ quote ident)
-     else case try (unprefix conjecture_prefix) ident of
-       SOME s =>
-       let val j = the (Int.fromString s) in
-         Isa_Raw (if j = length clauses then TrueI
-                  else Meson.make_meta_clause (nth clauses j))
-       end
-     | NONE => Isa_Raw TrueI)
+    let
+      fun some isa =
+        SOME (phi |> metis_literals_from_atp |> Metis_LiteralSet.fromList
+                  |> Metis_Thm.axiom, isa)
+    in
+      if ident = type_tag_idempotence_helper_name orelse
+         String.isPrefix lightweight_tags_sym_formula_prefix ident then
+        Isa_Reflexive_or_Trivial |> some
+      else if String.isPrefix helper_prefix ident then
+        case space_explode "_" ident  of
+          _ :: const :: j :: _ =>
+          nth (AList.lookup (op =) helper_table const |> the |> snd)
+              (the (Int.fromString j) - 1)
+          |> prepare_helper |> Isa_Raw |> some
+        | _ => raise Fail ("malformed helper identifier " ^ quote ident)
+      else case try (unprefix conjecture_prefix) ident of
+        SOME s =>
+        let val j = the (Int.fromString s) in
+          if j = length clauses then NONE
+          else Meson.make_meta_clause (nth clauses j) |> Isa_Raw |> some
+        end
+      | NONE => TrueI |> Isa_Raw |> some
+    end
   | metis_axiom_from_atp _ _ = raise Fail "not CNF -- expected formula"
 
 val default_type_sys = Preds (Polymorphic, Nonmonotonic_Types, Lightweight)
@@ -359,7 +363,7 @@
         prepare_atp_problem ctxt CNF Hypothesis Axiom type_sys explicit_apply
                             false false (map prop_of clauses) @{prop False} []
       val axioms =
-        atp_problem |> maps (map (metis_axiom_from_atp clauses) o snd)
+        atp_problem |> maps (map_filter (metis_axiom_from_atp clauses) o snd)
     in
       (MX, sym_tab,
        {axioms = axioms, tfrees = [], old_skolems = [] (* FIXME ### *)})