# HG changeset patch
# User bulwahn
# Date 1315572230 -7200
# Node ID f4a6786057d9cd39aedbbae361ff4a4adc4809c2
# Parent  0b3d3570ab3134c0cf3732f1d8bece86b28da81f
stating more explicitly our expectation that these two terms have the same term structure

diff -r 0b3d3570ab31 -r f4a6786057d9 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Fri Sep 09 12:33:09 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Fri Sep 09 14:43:50 2011 +0200
@@ -596,7 +596,9 @@
     end
   | annotate_term (Abs (_, _, t1) , Abs (x, T, t)) tvar_names =
     apfst (fn t => Abs (x, T, t)) (annotate_term (t1, t) tvar_names)
-  | annotate_term (_, t) tvar_names = (t, tvar_names)
+  | annotate_term (Free _, t as Free _) tvar_names = (t, tvar_names)
+  | annotate_term (Var _, t as Var _) tvar_names = (t, tvar_names)
+  | annotate_term (Bound   _, t as Bound _) tvar_names = (t, tvar_names)
 
 fun annotate_eqns thy (c, ty) eqns = 
   let