src/Pure/Isar/proof_context.ML
changeset 18928 042608ffa2ec
parent 18900 e7d4e51bd4b1
child 18953 93903be7ff66
--- a/src/Pure/Isar/proof_context.ML	Mon Feb 06 11:00:24 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Feb 06 11:01:28 2006 +0100
@@ -1115,7 +1115,7 @@
     val (ys, zs) = split_list (fixes_of ctxt);
     val (vars, ctxt') = prep raw_vars ctxt;
     val xs = map #1 vars;
-    val _ = no_dups ctxt (duplicates xs);
+    val _ = no_dups ctxt (gen_duplicates (op =) xs);
     val xs' =
       if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs)
       else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs);