# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1312650470 14400
# Node ID a8a538800278241acd95d4a4f06a985589141ce1
# Parent  7770ef82c46358d7631489772f749e79846f5bce
Better wildification, avoiding some unintentional variable capture

diff -r 7770ef82c463 -r a8a538800278 src/elaborate.sml
--- a/src/elaborate.sml	Thu Aug 04 17:06:50 2011 -0400
+++ b/src/elaborate.sml	Sat Aug 06 13:07:50 2011 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2008-2010, Adam Chlipala
+(* Copyright (c) 2008-2011, Adam Chlipala
  * All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
@@ -3380,8 +3380,12 @@
                        | L'.KRel _ => NONE
                        | L'.KFun _ => NONE
 
-                 fun decompileCon env (c, loc) =
-                     case c of
+                 fun maybeHnorm env c =
+                     hnormCon env c
+                     handle E.UnboundNamed _ => c
+
+                 fun decompileCon env (c as (_, loc)) =
+                     case #1 (maybeHnorm env c) of
                          L'.CRel i =>
                          let
                              val (s, _) = E.lookupCRel env i