# HG changeset patch
# User blanchet
# Date 1412615956 -7200
# Node ID c9e8ad426ab1a634d92627ecb0cbc9044205451e
# Parent  733b7a3277b2b0182e5cfc1b3b2ff719e5e63218
get rid of 'individual' type in DFG proofs

diff -r 733b7a3277b2 -r c9e8ad426ab1 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -96,6 +96,7 @@
   val tptp_true : string
   val tptp_lambda : string
   val tptp_empty_list : string
+  val dfg_individual_type : string
   val isabelle_info_prefix : string
   val isabelle_info : string -> int -> (string, 'a) atp_term list
   val extract_isabelle_status : (string, 'a) atp_term list -> string option
@@ -251,6 +252,9 @@
 val tptp_true = "$true"
 val tptp_lambda = "^"
 val tptp_empty_list = "[]"
+
+val dfg_individual_type = "iii" (* cannot clash *)
+
 val isabelle_info_prefix = "isabelle_"
 
 val inductionN = "induction"
@@ -386,8 +390,6 @@
   | uncurry_type _ =
     raise Fail "unexpected higher-order type in first-order format"
 
-val dfg_individual_type = "iii" (* cannot clash *)
-
 val suffix_type_of_types = suffix (" " ^ tptp_has_type ^ " " ^ tptp_type_of_types)
 
 fun str_of_type format ty =
diff -r 733b7a3277b2 -r c9e8ad426ab1 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -350,7 +350,9 @@
 
 (* We currently half ignore types. *)
 fun parse_optional_type_signature x =
-  Scan.option ($$ tptp_has_type |-- parse_type) x
+  (Scan.option ($$ tptp_has_type |-- parse_type)
+   >> (fn some as SOME (AType ((s, []), [])) => if s = dfg_individual_type then NONE else some
+        | res => res)) x
 and parse_arg x =
   ($$ "(" |-- parse_term --| $$ ")" --| parse_optional_type_signature
    || scan_general_id -- parse_optional_type_signature
@@ -519,7 +521,7 @@
   | remove_thf_app (AAbs (((x, ty), arg), t)) = AAbs (((x, ty), remove_thf_app arg), t)
 
 fun parse_thf0_typed_var x =
-  (Scan.repeat (scan_general_id -- Scan.option ($$ ":" |-- parse_thf0_type)
+  (Scan.repeat (scan_general_id -- Scan.option ($$ tptp_has_type |-- parse_thf0_type)
      --| Scan.option (Scan.this_string ","))
    || $$ "(" |-- parse_thf0_typed_var --| $$ ")") x
 
@@ -535,7 +537,8 @@
                     else I))
             ys t)
   || Scan.this_string tptp_not |-- parse_thf0_term >> mk_app (mk_simple_aterm tptp_not)
-  || scan_general_id --| $$ ":" -- parse_thf0_type >> (fn (var, typ) => ATerm ((var, [typ]), []))
+  || scan_general_id --| $$ tptp_has_type -- parse_thf0_type
+    >> (fn (var, typ) => ATerm ((var, [typ]), []))
   || parse_ho_quantifier >> mk_simple_aterm
   || $$ "(" |-- parse_thf0_term --| $$ ")"
   || scan_general_id >> mk_simple_aterm
diff -r 733b7a3277b2 -r c9e8ad426ab1 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Oct 06 19:19:16 2014 +0200
@@ -134,9 +134,7 @@
 fun var_name_of_typ (Type (@{type_name fun}, [_, T])) =
     if body_type T = HOLogic.boolT then "p" else "f"
   | var_name_of_typ (Type (@{type_name set}, [T])) =
-    let
-      fun default () = single_letter true (var_name_of_typ T)
-    in
+    let fun default () = single_letter true (var_name_of_typ T) in
       (case T of
         Type (s, [T1, T2]) => if String.isSuffix "prod" s andalso T1 = T2 then "r" else default ()
       | _ => default ())