# HG changeset patch
# User wenzelm
# Date 1158343717 -7200
# Node ID 4c1068697159b31f7966d834d03150502f028dd0
# Parent  893e7a9546ff2997f13a8cf451872963bedf017f
instantiate: omit has_duplicates check, which is irrelevant for soundness;

diff -r 893e7a9546ff -r 4c1068697159 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Sep 15 18:06:51 2006 +0200
+++ b/src/Pure/thm.ML	Fri Sep 15 20:08:37 2006 +0200
@@ -1087,19 +1087,14 @@
         val (tpairs', maxidx') =
           fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
       in
-        if has_duplicates (fn ((v, _), (v', _)) => Term.eq_var (v, v')) inst' then
-          raise THM ("instantiate: variables not distinct", 0, [th])
-        else if has_duplicates (fn ((v, _), (v', _)) => Term.eq_tvar (v, v')) instT' then
-          raise THM ("instantiate: type variables not distinct", 0, [th])
-        else
-          Thm {thy_ref = thy_ref',
-            der = Pt.infer_derivs' (fn d =>
-              Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
-            maxidx = maxidx',
-            shyps = shyps',
-            hyps = hyps,
-            tpairs = tpairs',
-            prop = prop'}
+        Thm {thy_ref = thy_ref',
+          der = Pt.infer_derivs' (fn d =>
+            Pt.instantiate (map (apsnd #1) instT', map (apsnd #1) inst') d) der,
+          maxidx = maxidx',
+          shyps = shyps',
+          hyps = hyps,
+          tpairs = tpairs',
+          prop = prop'}
       end
       handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);