1.1 --- a/src/Pure/sign.ML Sat Jun 14 17:26:12 2008 +0200
1.2 +++ b/src/Pure/sign.ML Sat Jun 14 17:26:14 2008 +0200
1.3 @@ -366,6 +366,8 @@
1.4
1.5 fun check_vars (t $ u) = (check_vars t; check_vars u)
1.6 | check_vars (Abs (_, _, t)) = check_vars t
1.7 + | check_vars (Free (x, _)) =
1.8 + if NameSpace.is_qualified x then err ("Malformed variable: " ^ quote x) else ()
1.9 | check_vars (Var (xi as (_, i), _)) =
1.10 if i < 0 then err ("Malformed variable: " ^ quote (Term.string_of_vname xi)) else ()
1.11 | check_vars _ = ();