# HG changeset patch
# User haftmann
# Date 1238144712 -3600
# Node ID 8a854c90f7e61b0a35effc47134341b2c84a2409
# Parent  0842e906300cd31055b2500162f2dd1c70deedc0
more convenient name uniqueness

diff -r 0842e906300c -r 8a854c90f7e6 src/Pure/Isar/code_unit.ML
--- a/src/Pure/Isar/code_unit.ML	Fri Mar 27 10:05:11 2009 +0100
+++ b/src/Pure/Isar/code_unit.ML	Fri Mar 27 10:05:12 2009 +0100
@@ -215,9 +215,10 @@
           |> Conjunction.elim_balanced (length thms)
   in
     thms
-    |> burrow_thms (canonical_tvars thy purify_tvar)
     |> map (canonical_vars thy purify_var)
     |> map (canonical_absvars purify_var)
+    |> map Drule.zero_var_indexes
+    |> burrow_thms (canonical_tvars thy purify_tvar)
     |> Drule.zero_var_indexes_list
   end;