src/Pure/Isar/calculation.ML

--- a/src/Pure/Isar/calculation.ML	Mon Oct 09 02:19:49 2006 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Oct 09 02:19:51 2006 +0200
@@ -85,7 +85,7 @@
 
 val symmetric = Thm.rule_attribute (fn x => fn th =>
   (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of
-    ([th'], _) => th'
+    ([th'], _) => Drule.zero_var_indexes th'
   | ([], _) => raise THM ("symmetric: no unifiers", 1, [th])
   | _ => raise THM ("symmetric: multiple unifiers", 1, [th])));