# HG changeset patch
# User bulwahn
# Date 1315396298 -7200
# Node ID 238c6c7da908d57e0f0372bed91c2b7800f2ca73
# Parent  d3fdd0a24e15566e07c6b0a497e55e4ecf7c3cf9
setting const_sorts to false in the type inference of the code generator

diff -r d3fdd0a24e15 -r 238c6c7da908 src/Tools/Code/code_thingol.ML
--- 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)) =