# HG changeset patch
# User blanchet
# Date 1284637937 -7200
# Node ID c6b21584f33641a2921b1c4f419a1c371a50c922
# Parent  acb25e9cf6fb9da92d16ac2958c30d04acb2b9d7
merge constructors

diff -r acb25e9cf6fb -r c6b21584f336 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 13:44:41 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Sep 16 13:52:17 2010 +0200
@@ -11,7 +11,7 @@
   type 'a fo_term = 'a ATP_Problem.fo_term
   type 'a uniform_formula = 'a ATP_Problem.uniform_formula
 
-  datatype step_name = Str of string * string | Num of string
+  type step_name = string * string option
 
   datatype 'a step =
     Definition of step_name * 'a * 'a |
@@ -19,7 +19,6 @@
 
   type 'a proof = 'a uniform_formula step list
 
-  val step_num : step_name -> string
   val is_same_step : step_name * step_name -> bool
   val atp_proof_from_tstplike_string : string -> string proof
   val map_term_names_in_atp_proof :
@@ -58,15 +57,12 @@
   | mk_anot phi = AConn (ANot, [phi])
 fun mk_aconn c (phi1, phi2) = AConn (c, [phi1, phi2])
 
-datatype step_name = Str of string * string | Num of string
+type step_name = string * string option
 
-fun step_num (Str (num, _)) = num
-  | step_num (Num num) = num
-
-val is_same_step = op = o pairself step_num
+fun is_same_step p = p |> pairself fst |> op =
 
 fun step_name_ord p =
-  let val q = pairself step_num p in
+  let val q = pairself fst p in
     (* The "unprefix" part is to cope with remote Vampire's output. The proper
        solution would be to perform a topological sort, e.g. using the nice
        "Graph" functor. *)
@@ -162,8 +158,8 @@
           let
             val (name, deps) =
               case deps of
-                ["file", _, s] => (Str (num, s), [])
-              | _ => (Num num, deps)
+                ["file", _, s] => ((num, SOME s), [])
+              | _ => ((num, NONE), deps)
           in
             case role of
               "definition" =>
@@ -172,9 +168,9 @@
                  Definition (name, phi1, phi2)
                | AAtom (ATerm ("c_equal", _)) =>
                  (* Vampire's equality proxy axiom *)
-                 Inference (name, phi, map Num deps)
+                 Inference (name, phi, map (rpair NONE) deps)
                | _ => raise Fail "malformed definition")
-            | _ => Inference (name, phi, map Num deps)
+            | _ => Inference (name, phi, map (rpair NONE) deps)
           end)
 
 (**** PARSING OF VAMPIRE OUTPUT ****)
@@ -182,7 +178,8 @@
 (* Syntax: <num>. <formula> <annotation> *)
 val parse_vampire_line =
   scan_general_id --| $$ "." -- parse_formula -- parse_annotation true
-  >> (fn ((num, phi), deps) => Inference (Num num, phi, map Num deps))
+  >> (fn ((num, phi), deps) =>
+         Inference ((num, NONE), phi, map (rpair NONE) deps))
 
 (**** PARSING OF SPASS OUTPUT ****)
 
@@ -217,7 +214,7 @@
 val parse_spass_line =
   scan_general_id --| $$ "[" --| $$ "0" --| $$ ":" --| Symbol.scan_id
     -- parse_spass_annotations --| $$ "]" -- parse_horn_clause --| $$ "."
-  >> (fn ((num, deps), u) => Inference (Num num, u, map Num deps))
+  >> (fn ((num, deps), u) => Inference ((num, NONE), u, map (rpair NONE) deps))
 
 val parse_line = parse_tstp_line || parse_vampire_line || parse_spass_line
 val parse_proof =
diff -r acb25e9cf6fb -r c6b21584f336 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 13:44:41 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Thu Sep 16 13:52:17 2010 +0200
@@ -68,13 +68,13 @@
       "\nTo minimize the number of lemmas, try this: " ^
       Markup.markup Markup.sendback command ^ "."
 
-fun resolve_axiom axiom_names (Str (_, s)) =
+fun resolve_axiom axiom_names ((_, SOME s)) =
     (case strip_prefix_and_unascii axiom_prefix s of
        SOME s' => (case find_first_in_list_vector axiom_names s' of
                      SOME x => [(s', x)]
                    | NONE => [])
      | NONE => [])
-  | resolve_axiom axiom_names (Num num) =
+  | resolve_axiom axiom_names (num, NONE) =
     case Int.fromString num of
       SOME j =>
       if j > 0 andalso j <= Vector.length axiom_names then
@@ -152,17 +152,15 @@
 val assum_prefix = "A"
 val fact_prefix = "F"
 
-fun resolve_conjecture conjecture_shape (Str (num, s)) =
-    let
-      val k = case try (unprefix conjecture_prefix) s of
-                SOME s => Int.fromString s |> the_default ~1
-              | NONE => case Int.fromString num of
-                          SOME j => find_index (exists (curry (op =) j))
-                                               conjecture_shape
-                        | NONE => ~1
-    in if k >= 0 then [k] else [] end
-  | resolve_conjecture conjecture_shape (Num num) =
-    resolve_conjecture conjecture_shape (Str (num, "")) (* HACK *)
+fun resolve_conjecture conjecture_shape (num, s_opt) =
+  let
+    val k = case try (unprefix conjecture_prefix) (the_default "" s_opt) of
+              SOME s => Int.fromString s |> the_default ~1
+            | NONE => case Int.fromString num of
+                        SOME j => find_index (exists (curry (op =) j))
+                                             conjecture_shape
+                      | NONE => ~1
+  in if k >= 0 then [k] else [] end
 
 val is_axiom = not o null oo resolve_axiom
 val is_conjecture = not o null oo resolve_conjecture
@@ -170,9 +168,9 @@
 fun raw_label_for_name conjecture_shape name =
   case resolve_conjecture conjecture_shape name of
     [j] => (conjecture_prefix, j)
-  | _ => case Int.fromString (step_num name) of
+  | _ => case Int.fromString (fst name) of
            SOME j => (raw_prefix, j)
-         | NONE => (raw_prefix ^ step_num name, 0)
+         | NONE => (raw_prefix ^ fst name, 0)
 
 (**** INTERPRETATION OF TSTP SYNTAX TREES ****)