# 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;