# HG changeset patch
# User wenzelm
# Date 1150143278 -7200
# Node ID e93ffc043dfde398c4d6c3779fab049ac0a3cb9d
# Parent  474cc9b49239cf7396f479f22a0e5337dad359b1
tuned;

diff -r 474cc9b49239 -r e93ffc043dfd src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Jun 12 21:19:07 2006 +0200
+++ b/src/HOL/Finite_Set.thy	Mon Jun 12 22:14:38 2006 +0200
@@ -499,10 +499,9 @@
 text{* Interpretation of locales: *}
 
 interpretation AC_add: ACe ["op +" "0::'a::comm_monoid_add"]
-by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
+  by(auto intro: ACf.intro ACe_axioms.intro add_assoc add_commute)
 
 interpretation AC_mult: ACe ["op *" "1::'a::comm_monoid_mult"]
-  apply -
    apply (fast intro: ACf.intro mult_assoc mult_commute)
   apply (fastsimp intro: ACe_axioms.intro mult_assoc mult_commute)
   done
@@ -511,7 +510,7 @@
 subsubsection{*From @{term foldSet} to @{term fold}*}
 
 lemma image_less_Suc: "h ` {i. i < Suc m} = insert (h m) (h ` {i. i < m})"
-by (auto simp add: less_Suc_eq) 
+  by (auto simp add: less_Suc_eq) 
 
 lemma insert_image_inj_on_eq:
      "[|insert (h m) A = h ` {i. i < Suc m}; h m \<notin> A; 
diff -r 474cc9b49239 -r e93ffc043dfd src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Mon Jun 12 21:19:07 2006 +0200
+++ b/src/Pure/Tools/invoke.ML	Mon Jun 12 22:14:38 2006 +0200
@@ -69,20 +69,16 @@
           val params'' = map (Thm.term_of o Drule.dest_term) res_params;
           val elems' = elems |> map (Element.inst_ctxt thy
             (Symtab.make (map #1 types ~~ types''), Symtab.make (map #1 params ~~ params'')));
+          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
 
-          val prems'' = map2 Element.make_witness (maps Element.prems_of elems') res_prems;
           val Element.Notes notes = 
             Element.Notes (maps (Element.facts_of thy) elems')
             |> Element.satisfy_ctxt prems''
             |> Element.map_ctxt_values I I (ProofContext.export ctxt'' ctxt);
-              (* FIXME export typs/terms *)
-
-          val _ = print notes;
-
+            (* FIXME export typs/terms *)
           val notes' = notes
             |> Attrib.map_facts (Attrib.attribute_i thy)
             |> map (fn ((a, atts), facts) => ((a, atts @ more_atts), facts));
-
         in
           ctxt
           |> ProofContext.sticky_prefix prfx
@@ -92,7 +88,7 @@
         end) #> Proof.put_facts NONE);
   in
     state'
-    |> Proof.local_goal (ProofDisplay.print_results int) (K I) ProofContext.bind_propp_schematic_i
+    |> Proof.local_goal (K (K ())) (K I) ProofContext.bind_propp_schematic_i
       "invoke" NONE after_qed propp
     |> Element.refine_witness
     |> Seq.hd