src/Tools/Code/code_thingol.ML
changeset 32929 0e9e13ac06d7
parent 32928 6bcc35f7ff6d
child 33029 2fefe039edf1
     1.1 --- a/src/Tools/Code/code_thingol.ML	Wed Oct 14 12:20:01 2009 +0200
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Oct 14 13:56:56 2009 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4    in Thm.certify_instantiate ([], var_subst) thm end;
     1.5  
     1.6  fun canonize_thms thy = map (Thm.transfer thy)
     1.7 -  #> Code.same_typscheme thy #> desymbolize_tvars thy
     1.8 +  #> Code.standard_typscheme thy #> desymbolize_tvars thy
     1.9    #> same_arity thy #> map (desymbolize_vars thy);
    1.10  
    1.11