Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Added well-formedness check to Abst case in function prf_of.
authorberghofe
Tue, 30 Oct 2007 17:56:56 +0100
changeset 25245 1fcfcdcba53c
parent 25244 42071ca3a14c
child 25246 584d8f2e1fc9
Added well-formedness check to Abst case in function prf_of.
src/Pure/Proof/proof_syntax.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle