- Tuned function mk_cnstrts
- Added function prop_of

--- a/src/Pure/Proof/reconstruct.ML	Fri May 10 22:53:53 2002 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Sat May 11 20:27:13 2002 +0200
@@ -10,6 +10,7 @@
 sig
   val quiet_mode : bool ref
   val reconstruct_proof : Sign.sg -> term -> Proofterm.proof -> Proofterm.proof
+  val prop_of : Proofterm.proof -> term
   val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
 end;
 
@@ -129,13 +130,15 @@
             cantunify sg (Envir.norm_term env t') (Envir.norm_term env u')
       end;
 
-    fun mk_cnstrts_atom env ts prop opTs mk_prf =
+    fun mk_cnstrts_atom env ts prop opTs prf =
           let
             val tvars = term_tvars prop;
             val (env', Ts) = if_none (apsome (pair env) opTs)
               (foldl_map (mk_tvar o apsnd snd) (env, tvars));
-            val prop' = subst_TVars (map fst tvars ~~ Ts) (forall_intr_vfs prop);
-          in (prop', mk_prf (Some Ts), [], env', ts) end;
+            val prop' = subst_TVars (map fst tvars ~~ Ts) (forall_intr_vfs prop)
+              handle LIST _ => error ("Wrong number of type arguments for " ^
+                quote (fst (get_name_tags [] prop prf)))
+          in (prop', change_type (Some Ts) prf, [], env', ts) end;
 
     fun mk_cnstrts env _ Hs ts (PBound i) = (nth_elem (i, Hs), PBound i, [], env, ts)
       | mk_cnstrts env Ts Hs ts (Abst (s, Some T, cprf)) =
@@ -201,12 +204,12 @@
                  add_cnstrt Ts (v $ t) (prf % Some t) cnstrts env3 ts'
                    (u, Const ("all", (T --> propT) --> propT) $ v)
                end)
-      | mk_cnstrts env _ _ ts (PThm (name, prf, prop, opTs)) =
-          mk_cnstrts_atom env ts prop opTs (fn x => PThm (name, prf, prop, x))
-      | mk_cnstrts env _ _ ts (PAxm (name, prop, opTs)) =
-          mk_cnstrts_atom env ts prop opTs (fn x => PAxm (name, prop, x))
-      | mk_cnstrts env _ _ ts (Oracle (name, prop, opTs)) =
-          mk_cnstrts_atom env ts prop opTs (fn x => Oracle (name, prop, x))
+      | mk_cnstrts env _ _ ts (prf as PThm (_, _, prop, opTs)) =
+          mk_cnstrts_atom env ts prop opTs prf
+      | mk_cnstrts env _ _ ts (prf as PAxm (_, prop, opTs)) =
+          mk_cnstrts_atom env ts prop opTs prf
+      | mk_cnstrts env _ _ ts (prf as Oracle (_, prop, opTs)) =
+          mk_cnstrts_atom env ts prop opTs prf
       | mk_cnstrts env _ _ ts (Hyp t) = (t, Hyp t, [], env, ts)
       | mk_cnstrts _ _ _ _ _ = error "reconstruct_proof: minimal proof object"
   in mk_cnstrts env [] [] ts cprf end;
@@ -299,6 +302,30 @@
     thawf (norm_proof env' prf)
   end;
 
+fun prop_of prf =
+  let
+    fun prop_of_atom prop Ts =
+      subst_TVars (map fst (term_tvars prop) ~~ Ts) (forall_intr_vfs prop);
+
+    fun prop_of' Hs (PBound i) = nth_elem (i, Hs)
+      | prop_of' Hs (Abst (s, Some T, prf)) =
+          all T $ (Abs (s, T, prop_of' Hs prf))
+      | prop_of' Hs (AbsP (s, Some t, prf)) =
+          Logic.mk_implies (t, prop_of' (t :: Hs) prf)
+      | prop_of' Hs (prf % Some t) = (case prop_of' Hs prf of
+          Const ("all", _) $ f => betapply (f, t)
+        | _ => error "prop_of: all expected")
+      | prop_of' Hs (prf1 %% prf2) = (case prop_of' Hs prf1 of
+          Const ("==>", _) $ P $ Q => Q
+        | _ => error "prop_of: ==> expected")
+      | prop_of' Hs (Hyp t) = t
+      | prop_of' Hs (PThm (_, _, prop, Some Ts)) = prop_of_atom prop Ts
+      | prop_of' Hs (PAxm (_, prop, Some Ts)) = prop_of_atom prop Ts
+      | prop_of' Hs (Oracle (_, prop, Some Ts)) = prop_of_atom prop Ts
+      | prop_of' _ _ = error "prop_of: partial proof object";
+
+  in prop_of' [] prf end;
+
 
 (********************************************************************************
   expand and reconstruct subproofs