# HG changeset patch
# User wenzelm
# Date 1213457174 -7200
# Node ID 56c96c02ab79f4c16274b6b2b8120b8bbc157788
# Parent  eed29f78dd9be9f3e57f072260497400d551542a
certify_term: reject qualified frees;

diff -r eed29f78dd9b -r 56c96c02ab79 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sat Jun 14 17:26:12 2008 +0200
+++ b/src/Pure/sign.ML	Sat Jun 14 17:26:14 2008 +0200
@@ -366,6 +366,8 @@
 
 fun check_vars (t $ u) = (check_vars t; check_vars u)
   | check_vars (Abs (_, _, t)) = check_vars t
+  | check_vars (Free (x, _)) =
+      if NameSpace.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
   | check_vars (Var (xi as (_, i), _)) =
       if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
   | check_vars _ = ();