1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:19 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:21 2011 +0200
     1.3 @@ -589,27 +589,16 @@
     1.4  fun annotate_term (proj_sort, _) eqngr =
     1.5    let
     1.6      val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr
     1.7 -    fun annotate (Const (c', T'), Const (c, T)) tvar_names =
     1.8 -      let
     1.9 -        val tvar_names' = Term.add_tvar_namesT T' tvar_names
    1.10 -      in
    1.11 -        if not (eq_set (op =) (tvar_names, tvar_names')) andalso has_sort_constraints c then
    1.12 -          (Const (c, Type ("", [T])), tvar_names')
    1.13 +    fun annotate (Const (c', T'), Const (c, T)) =
    1.14 +        if not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c then
    1.15 +          Const (c, Type ("", [T]))
    1.16          else
    1.17 -          (Const (c, T), tvar_names)
    1.18 -      end
    1.19 -      | annotate (t1 $ u1, t $ u) tvar_names =
    1.20 -      let
    1.21 -        val (u', tvar_names') = annotate (u1, u) tvar_names
    1.22 -        val (t', tvar_names'') = annotate (t1, t) tvar_names'    
    1.23 -      in
    1.24 -        (t' $ u', tvar_names'')
    1.25 -      end
    1.26 -      | annotate (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
    1.27 -        apfst (fn t => Abs (x, T, t)) (annotate (t1, t) tvar_names)
    1.28 -      | annotate (Free _, t as Free _) tvar_names = (t, tvar_names)
    1.29 -      | annotate (Var _, t as Var _) tvar_names = (t, tvar_names)
    1.30 -      | annotate (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
    1.31 +          Const (c, T)
    1.32 +      | annotate (t1 $ u1, t $ u) = annotate (t1, t) $ annotate (u1, u)
    1.33 +      | annotate (Abs (_, _, t1) , Abs (x, T, t)) = Abs (x, T, annotate (t1, t))
    1.34 +      | annotate (Free _, t as Free _) = t
    1.35 +      | annotate (Var _, t as Var _) = t
    1.36 +      | annotate (Bound   _, t as Bound _) = t
    1.37    in
    1.38      annotate
    1.39    end
    1.40 @@ -622,7 +611,7 @@
    1.41      val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
    1.42      val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
    1.43    in
    1.44 -    fst (annotate_term algbr eqngr (reinferred_rhs, rhs) [])
    1.45 +    annotate_term algbr eqngr (reinferred_rhs, rhs)
    1.46    end
    1.47  
    1.48  fun annotate_eqns thy algbr eqngr (c, ty) eqns =