# HG changeset patch
# User bulwahn
# Date 1315396294 -7200
# Node ID 7ecb4124a3a3935b6925401c7d9faa89fe8a4cce
# Parent  c13fdf710a40a7c9b6be8bca56960c2e232f87ab
adding call to disambiguation annotations

diff -r c13fdf710a40 -r 7ecb4124a3a3 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
@@ -611,7 +611,6 @@
 
 (* inference of type annotations for disambiguation with type classes *)
 
-
 fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
     let
       val tvar_names' = Term.add_tvar_namesT T' tvar_names
@@ -671,11 +670,12 @@
     fun stmt_fun cert =
       let
         val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
+        val eqns' = annotate_eqns thy eqns
         val some_case_cong = Code.get_case_cong thy c;
       in
         fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
         ##>> translate_typ thy algbr eqngr permissive ty
-        ##>> translate_eqns thy algbr eqngr permissive eqns
+        ##>> translate_eqns thy algbr eqngr permissive eqns'
         #>> (fn info => Fun (c, (info, some_case_cong)))
       end;
     val stmt_const = case Code.get_type_of_constr_or_abstr thy c