# HG changeset patch
# User blanchet
# Date 1306916983 -7200
# Node ID 9e9420122f91b7865d788b72380cc24ca3b115af
# Parent  d73fc2e553085ada2a6fa7418d6bd84a449da57e
fixed interaction between type tags and hAPP in reconstruction code

diff -r d73fc2e55308 -r 9e9420122f91 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 01 10:29:43 2011 +0200
@@ -423,7 +423,7 @@
   let
     (* see also "mk_var" in "Metis_Reconstruct" *)
     val var_index = if textual then 0 else 1
-    fun do_term extra_us opt_T u =
+    fun do_term extra_ts opt_T u =
       case u of
         ATerm (a, us) =>
         if String.isPrefix simple_type_prefix a then
@@ -445,12 +445,18 @@
             if s' = type_tag_name then
               case mangled_us @ us of
                 [typ_u, term_u] =>
-                do_term extra_us (SOME (typ_from_atp tfrees typ_u)) term_u
+                do_term extra_ts (SOME (typ_from_atp tfrees typ_u)) term_u
               | _ => raise FO_TERM us
             else if s' = predicator_name then
               do_term [] (SOME @{typ bool}) (hd us)
             else if s' = app_op_name then
-              do_term (List.last us :: extra_us) opt_T (nth us (length us - 2))
+              let val extra_t = do_term [] NONE (List.last us) in
+                do_term (extra_t :: extra_ts)
+                        (case opt_T of
+                           SOME T => SOME (fastype_of extra_t --> T)
+                         | NONE => NONE)
+                        (nth us (length us - 2))
+              end
             else if s' = type_pred_name then
               @{const True} (* ignore type predicates *)
             else
@@ -459,24 +465,21 @@
                   length us - the_default 0 (Symtab.lookup sym_tab s)
                 val (type_us, term_us) =
                   chop num_ty_args us |>> append mangled_us
-                (* Extra args from "hAPP" come after any arguments given
-                   directly to the constant. *)
                 val term_ts = map (do_term [] NONE) term_us
-                val extra_ts = map (do_term [] NONE) extra_us
                 val T =
                   if not (null type_us) andalso
                      num_type_args thy s' = length type_us then
                     (s', map (typ_from_atp tfrees) type_us)
                     |> Sign.const_instance thy
                   else case opt_T of
-                    SOME T => map fastype_of (term_ts @ extra_ts) ---> T
+                    SOME T => map fastype_of term_ts ---> T
                   | NONE => HOLogic.typeT
                 val s' = s' |> unproxify_const
               in list_comb (Const (s', T), term_ts @ extra_ts) end
           end
         | NONE => (* a free or schematic variable *)
           let
-            val ts = map (do_term [] NONE) (us @ extra_us)
+            val ts = map (do_term [] NONE) us @ extra_ts
             val T = map fastype_of ts ---> HOLogic.typeT
             val t =
               case strip_prefix_and_unascii fixed_var_prefix a of
@@ -568,7 +571,7 @@
       | _ => raise FORMULA [phi]
   in repair_tvar_sorts (do_formula true phi Vartab.empty) end
 
-fun check_formula ctxt =
+fun infer_formula_types ctxt =
   Type.constraint HOLogic.boolT
   #> Syntax.check_term
          (Proof_Context.set_mode Proof_Context.mode_schematic ctxt)
@@ -588,7 +591,7 @@
       val t2 = prop_from_atp thy true sym_tab tfrees phi2
       val (t1, t2) =
         HOLogic.eq_const HOLogic.typeT $ t1 $ t2
-        |> unvarify_args |> uncombine_term thy |> check_formula ctxt
+        |> unvarify_args |> uncombine_term thy |> infer_formula_types ctxt
         |> HOLogic.dest_eq
     in
       (Definition (name, t1, t2),
@@ -598,7 +601,7 @@
     let
       val thy = Proof_Context.theory_of ctxt
       val t = u |> prop_from_atp thy true sym_tab tfrees
-                |> uncombine_term thy |> check_formula ctxt
+                |> uncombine_term thy |> infer_formula_types ctxt
     in
       (Inference (name, t, deps),
        fold Variable.declare_term (OldTerm.term_frees t) ctxt)