# HG changeset patch
# User ballarin
# Date 1096372489 -7200
# Node ID eb4343a0d5710e371d2164cf39578400d8789717
# Parent  5f54721547a7b42e5af044814e6f5e0b98e55fd8
Bug fixes.

diff -r 5f54721547a7 -r eb4343a0d571 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Tue Sep 28 10:44:51 2004 +0200
+++ b/src/Pure/Isar/locale.ML	Tue Sep 28 13:54:49 2004 +0200
@@ -444,7 +444,7 @@
       end;
 
     fun identify top (Locale name) =
-    (* CB: ids is a list of tuples of the form ((name, ps), axs),
+    (* CB: ids is a list of tuples of the form ((name, ps)  axs),
        where name is a locale name, ps a list of parameter names and axs
        a list of axioms relating to the identifier, axs is empty unless
        identify at top level (top = true);
@@ -942,8 +942,9 @@
 
     val (ctxt, (elemss, _)) =
       activate_facts prep_facts (import_ctxt, qs);
-    val stmt = gen_duplicates Term.aconv
-       (flat (map (fn ((_, axs), _) => flat (map (#hyps o Thm.rep_thm) axs)) qs));
+    val stmt = gen_distinct Term.aconv
+       (flat (map (fn ((_, axs), _) =>
+         flat (map (#hyps o Thm.rep_thm) axs)) qs));
     val cstmt = map (cterm_of sign) stmt;
   in
     ((((import_ctxt, import_elemss), (ctxt, elemss)), (parms, spec, defs)), (cstmt, concl))
diff -r 5f54721547a7 -r eb4343a0d571 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 28 10:44:51 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 28 13:54:49 2004 +0200
@@ -878,14 +878,6 @@
       (case kind of Theorem x => x | _ => err_malformed "finish_global" state);
 
     val ts = flat tss;
-val _ = set show_hyps;
-val _ = PolyML.print "finish_global";
-val _ = PolyML.print "ts:";
-val _ = PolyML.print ts;
-val _ = PolyML.print "raw_thm:";
-val _ = PolyML.print raw_thm;
-val _ = PolyML.print "elems_view";
-val _ = PolyML.print elems_view;
     val locale_results = map (ProofContext.export_standard elems_view goal_ctxt locale_ctxt)
       (prep_result state ts raw_thm);