1.1 --- a/src/Tools/Code/code_thingol.ML	Fri Sep 09 12:33:09 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Fri Sep 09 14:43:50 2011 +0200
     1.3 @@ -596,7 +596,9 @@
     1.4      end
     1.5    | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
     1.6      apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
     1.7 -  | annotate_term (_, t) tvar_names = (t, tvar_names)
     1.8 +  | annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names)
     1.9 +  | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
    1.10 +  | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
    1.11  
    1.12  fun annotate_eqns thy (c, ty) eqns = 
    1.13    let