adding call to disambiguation annotations
authorbulwahn
Wed Sep 07 13:51:34 2011 +0200 (2011-09-07)
changeset 447917ecb4124a3a3
parent 44790 c13fdf710a40
child 44792 26b19918e670
adding call to disambiguation annotations
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:34 2011 +0200
     1.3 @@ -611,7 +611,6 @@
     1.4  
     1.5  (* inference of type annotations for disambiguation with type classes *)
     1.6  
     1.7 -
     1.8  fun annotate_term (Const (c', T'), Const (c, T)) tvar_names =
     1.9      let
    1.10        val tvar_names' = Term.add_tvar_namesT T' tvar_names
    1.11 @@ -671,11 +670,12 @@
    1.12      fun stmt_fun cert =
    1.13        let
    1.14          val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
    1.15 +        val eqns' = annotate_eqns thy eqns
    1.16          val some_case_cong = Code.get_case_cong thy c;
    1.17        in
    1.18          fold_map (translate_tyvar_sort thy algbr eqngr permissive) vs
    1.19          ##>> translate_typ thy algbr eqngr permissive ty
    1.20 -        ##>> translate_eqns thy algbr eqngr permissive eqns
    1.21 +        ##>> translate_eqns thy algbr eqngr permissive eqns'
    1.22          #>> (fn info => Fun (c, (info, some_case_cong)))
    1.23        end;
    1.24      val stmt_const = case Code.get_type_of_constr_or_abstr thy c