--- 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)) =