certify_term: reject qualified frees;
authorwenzelm
Sat, 14 Jun 2008 17:26:14 +0200
changeset 2720556c96c02ab79
parent 27204 eed29f78dd9b
child 27206 9a786d5f8821
certify_term: reject qualified frees;
src/Pure/sign.ML
     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 _ = ();