# HG changeset patch
# User berghofe
# Date 1193763416 -3600
# Node ID 1fcfcdcba53cae191361bde4924e028c7376f29f
# Parent  42071ca3a14ccacc2ed7866ec57086ef2c461dfd
Added well-formedness check to Abst case in function prf_of.

diff -r 42071ca3a14c -r 1fcfcdcba53c src/Pure/Proof/proof_syntax.ML
--- a/src/Pure/Proof/proof_syntax.ML	Tue Oct 30 16:00:30 2007 +0100
+++ b/src/Pure/Proof/proof_syntax.ML	Tue Oct 30 17:56:56 2007 +0100
@@ -154,7 +154,9 @@
       | prf_of Ts (Const ("Hyp", _) $ prop) = Hyp prop
       | prf_of Ts (v as Var ((_, Type ("proof", _)))) = Hyp v
       | prf_of [] (Const ("Abst", _) $ Abs (s, T, prf)) =
-          Abst (s, if ty then SOME T else NONE,
+          if T = proofT then
+            error ("Term variable abstraction may not bind proof variable " ^ quote s)
+          else Abst (s, if ty then SOME T else NONE,
             incr_pboundvars (~1) 0 (prf_of [] prf))
       | prf_of [] (Const ("AbsP", _) $ t $ Abs (s, _, prf)) =
           AbsP (s, case t of