setting const_sorts to false in the type inference of the code generator

--- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:37 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:38 2011 +0200
@@ -607,7 +607,7 @@
 
 fun annotate_eqns thy eqns = 
   let
-    val ctxt = ProofContext.init_global thy
+    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)), (SOME th, proper)) =