# HG changeset patch
# User berghofe
# Date 1025286679 -7200
# Node ID cf85c4f7dcf272e473213583814d1c845c2dac9d
# Parent  407ad9c3036d04e07650684e5b263cdd7eed5ce8
Added function prop_of' taking assumption context as an argument.

diff -r 407ad9c3036d -r cf85c4f7dcf2 src/Pure/Proof/reconstruct.ML
--- a/src/Pure/Proof/reconstruct.ML	Fri Jun 28 17:36:22 2002 +0200
+++ b/src/Pure/Proof/reconstruct.ML	Fri Jun 28 19:51:19 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' : term list -> Proofterm.proof -> term
   val prop_of : Proofterm.proof -> term
   val expand_proof : Sign.sg -> string list -> Proofterm.proof -> Proofterm.proof
 end;
@@ -302,29 +303,27 @@
     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_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";
+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;
+val prop_of = prop_of' [];
 
 
 (********************************************************************************