# HG changeset patch
# User bulwahn
# Date 1316441898 -7200
# Node ID 410eea28b0f7a0cd2d45a0c388491823543c6204
# Parent  eff5bccc9b76beb1b9bf1ef71962fb47c7c07ca8
also adding type annotations for the dynamic invocation

diff -r eff5bccc9b76 -r 410eea28b0f7 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Sep 19 14:35:51 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Mon Sep 19 16:18:18 2011 +0200
@@ -600,22 +600,19 @@
   | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
   | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
 
-fun annotate_eqns thy (c, ty) eqns = 
+fun annotate thy (c, ty) args rhs =
   let
     val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
     val erase = map_types (fn _ => Type_Infer.anyT [])
     val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
-    fun add_annotations (args, (rhs, some_abs)) =
-      let
-        val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
-        val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
-        val (rhs', _) = annotate_term (reinferred_rhs, rhs) []
-     in
-        (args, (rhs', some_abs))
-     end
+    val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args)
+    val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))))
   in
-    map (apfst add_annotations) eqns
-  end;
+    fst (annotate_term (reinferred_rhs, rhs) [])
+  end
+
+fun annotate_eqns thy (c, ty) eqns = 
+  map (apfst (fn (args, (rhs, some_abs)) => (args, (annotate thy (c, ty) args rhs, some_abs)))) eqns
 
 (* translation *)
 
@@ -922,10 +919,11 @@
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
+    val t' = annotate thy (Term.dummy_patternN, ty) [] (Code.subst_signatures thy t) 
     val stmt_value =
       fold_map (translate_tyvar_sort thy algbr eqngr false) vs
       ##>> translate_typ thy algbr eqngr false ty
-      ##>> translate_term thy algbr eqngr false NONE (Code.subst_signatures thy t, NONE)
+      ##>> translate_term thy algbr eqngr false NONE (t', NONE)
       #>> (fn ((vs, ty), t) => Fun
         (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
     fun term_value (dep, (naming, program1)) =