src/Pure/Proof/reconstruct.ML

   let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
   in all T $ Abs (a, T, abstract_over (t, prop)) end;
 
 fun forall_intr_vfs prop = foldr forall_intr
   (vars_of prop @ sort (make_ord atless) (term_frees prop), prop);
+
+fun forall_intr_prf (t, prf) =
+  let val (a, T) = (case t of Var ((a, _), T) => (a, T) | Free p => p)
+  in Abst (a, Some T, prf_abstract_over t prf) end;
+
+fun forall_intr_vfs_prf prop prf = foldr forall_intr_prf
+  (vars_of prop @ sort (make_ord atless) (term_frees prop), prf);
 
 fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1})
   (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) =
     Envir.Envir {asol=Vartab.merge (op aconv) (asol1, asol2),
                  iTs=Vartab.merge (op =) (iTs1, iTs2),

   | decompose sg env Ts t u = (env, [(mk_abs Ts t, mk_abs Ts u)]);
 
 fun cantunify sg t u = error ("Non-unifiable terms:\n" ^
   Sign.string_of_term sg t ^ "\n\n" ^ Sign.string_of_term sg u);
 
+(*finds type of term without checking that combinations are consistent
+  rbinder holds types of bound variables*)
+fun fastype (Envir.Envir {iTs, ...}) =
+  let
+    fun devar (T as TVar (ixn, _)) = (case Vartab.lookup (iTs, ixn) of
+          None => T | Some U => devar U)
+      | devar T = T;
+    fun fast Ts (f $ u) = (case devar (fast Ts f) of
+           Type("fun",[_,T]) => T
+         | _ => raise TERM ("fastype: expected function type", [f $ u]))
+      | fast Ts (Const (_, T)) = T
+      | fast Ts (Free (_, T)) = T
+      | fast Ts (Bound i) =
+        (nth_elem (i, Ts)
+         handle LIST _=> raise TERM("fastype: Bound", [Bound i]))
+      | fast Ts (Var (_, T)) = T 
+      | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
+  in fast end;
+
 fun make_constraints_cprf sg env ts cprf =
   let
     fun add_cnstrt Ts prop prf cs env ts (t, u) =
       let
         val t' = mk_abs Ts t;
         val u' = mk_abs Ts u;
-        val nt = Envir.norm_term env t';
-        val nu = Envir.norm_term env u'
+        val nt = Envir.beta_norm t';
+        val nu = Envir.beta_norm u'
+
       in
-        if Pattern.pattern nt andalso Pattern.pattern nu then
-          let
-            val env' = (Pattern.unify (sg, env, [(nt, nu)]) handle Pattern.Unif =>
-                       cantunify sg nt nu);
-          in (Envir.norm_term env' prop, prf, cs, env', ts) end
-        else
-          let val (env', cs') = decompose sg env [] nt nu
-          in (Envir.norm_term env' prop, prf, cs @ cs', env', ts) end
+        ((prop, prf, cs, Pattern.unify (sg, env, [(nt, nu)]), ts)
+         handle Pattern.Pattern =>
+           let
+             val nt' = Envir.norm_term env nt;
+             val nu' = Envir.norm_term env nu
+           in
+             (prop, prf, cs, Pattern.unify (sg, env, [(nt', nu')]), ts)
+             handle Pattern.Pattern =>
+               let val (env', cs') = decompose sg env [] nt' nu'
+               in (prop, prf, cs @ cs', env', ts) end
+           end) handle Pattern.Unif =>
+        cantunify sg (Envir.norm_term env t') (Envir.norm_term env u')
       end;
 
     fun mk_cnstrts_atom env ts prop opTs mk_prf =
           let
             val tvars = term_tvars prop;

       | mk_cnstrts env Ts Hs (t::ts) (cprf % Some _) =
           let val t' = strip_abs Ts t
           in (case mk_cnstrts env Ts Hs ts cprf of
              (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ f,
                  prf, cnstrts, env', ts') =>
-               let val env'' = unifyT sg env' T
-                 (fastype_of1 (map (Envir.norm_type env') Ts, t'))
+               let val env'' = unifyT sg env' T (fastype env' Ts t')
                in (betapply (f, t'), prf % Some t', cnstrts, env'', ts')
                end
            | (u, prf, cnstrts, env', ts') =>
                let
-                 val T = fastype_of1 (map (Envir.norm_type env') Ts, t');
+                 val T = fastype env' Ts t';
                  val (env'', v) = mk_var env' Ts (T --> propT);
                in
                  add_cnstrt Ts (v $ t') (prf % Some t') cnstrts env'' ts'
                    (u, Const ("all", (T --> propT) --> propT) $ v)
                end)

 
 (********************************************************************************
   expand and reconstruct subproofs
 *********************************************************************************)
 
-fun full_forall_intr_proof prf x a T = Abst (a, Some T, prf_abstract_over x prf);
-
 fun expand_proof sg names prf =
   let
     fun expand prfs (AbsP (s, t, prf)) = 
           let val (prfs', prf') = expand prfs prf
           in (prfs', AbsP (s, t, prf')) end

             val (prf, prfs') = (case assoc (prfs, (a, prop)) of
                 None =>
                   let
                     val _ = message ("Reconstructing proof of " ^ a);
                     val _ = message (Sign.string_of_term sg prop);
-                    val prf = reconstruct_proof sg prop cprf
-                  in (prf, ((a, prop), prf)::prfs) end
+                    val (prfs', prf) = expand prfs (forall_intr_vfs_prf prop
+                      (reconstruct_proof sg prop cprf))
+                  in (prf, ((a, prop), prf) :: prfs') end
               | Some prf => (prf, prfs));
-            val tvars = term_tvars prop;
-            val vars = vars_of prop;
-            val tye = map fst tvars ~~ Ts;
-            fun abst (t as Var ((s, _), T), prf) = full_forall_intr_proof prf t s T;
-            val prf' = map_proof_terms (subst_TVars tye) (typ_subst_TVars tye) prf
+            val tye = map fst (term_tvars prop) ~~ Ts
           in
-            expand prfs' (foldr abst (map (subst_TVars tye) vars, prf'))
+            (prfs', map_proof_terms (subst_TVars tye) (typ_subst_TVars tye) prf)
           end
       | expand prfs prf = (prfs, prf);
 
   in snd (expand [] prf) end;