# HG changeset patch
# User blanchet
# Date 1307385395 -7200
# Node ID 649bada59658b3f31f80d3a14ab90c271d102194
# Parent  cd3b7798ecc2e9351bc558923b5a7a2b09e08a5d
slacker version of "fastype_of", in case a function has dummy type

diff -r cd3b7798ecc2 -r 649bada59658 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Mon Jun 06 20:36:35 2011 +0200
@@ -422,7 +422,9 @@
                    | NONE => s)
     | _ => s
   end
-  
+
+fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+
 (* First-order translation. No types are known for variables. "HOLogic.typeT"
    should allow them to be inferred. *)
 fun term_from_atp ctxt textual sym_tab =
@@ -460,7 +462,7 @@
               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)
+                           SOME T => SOME (slack_fastype_of extra_t --> T)
                          | NONE => NONE)
                         (nth us (length us - 2))
               end
@@ -479,7 +481,7 @@
                     (s', map (typ_from_atp ctxt) type_us)
                     |> Sign.const_instance thy
                   else case opt_T of
-                    SOME T => map fastype_of term_ts ---> T
+                    SOME T => map slack_fastype_of term_ts ---> T
                   | NONE => HOLogic.typeT
                 val s' = s' |> unproxify_const
               in list_comb (Const (s', T), term_ts @ extra_ts) end
@@ -487,7 +489,7 @@
         | NONE => (* a free or schematic variable *)
           let
             val ts = map (do_term [] NONE) us @ extra_ts
-            val T = map fastype_of ts ---> HOLogic.typeT
+            val T = map slack_fastype_of ts ---> HOLogic.typeT
             val t =
               case strip_prefix_and_unascii fixed_var_prefix a of
                 SOME b => Free (b, T)