setting const_sorts to false in the type inference of the code generator
authorbulwahn
Wed Sep 07 13:51:38 2011 +0200 (2011-09-07)
changeset 44795238c6c7da908
parent 44794 d3fdd0a24e15
child 44796 7f1f164696a4
setting const_sorts to false in the type inference of the code generator
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:37 2011 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:38 2011 +0200
     1.3 @@ -607,7 +607,7 @@
     1.4  
     1.5  fun annotate_eqns thy eqns = 
     1.6    let
     1.7 -    val ctxt = ProofContext.init_global thy
     1.8 +    val ctxt = ProofContext.init_global thy |> Config.put Type_Infer_Context.const_sorts false
     1.9      val erase = map_types (fn _ => Type_Infer.anyT [])
    1.10      val reinfer = singleton (Type_Infer_Context.infer_types ctxt)
    1.11      fun add_annotations ((args, (rhs, some_abs)), (SOME th, proper)) =