# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID 8c5d44c7e8af86863f3f1ddc183fece6d93c2d1e
# Parent  de9e0adc21dac89733c21d641e434d52842362bb
tuning: unused var

diff -r de9e0adc21da -r 8c5d44c7e8af src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -663,12 +663,12 @@
      THEN PRIMITIVE do_instantiate) st
   end
 
-fun fix_exists_tac thy t =
+fun fix_exists_tac t =
   etac @{thm exE}
   THEN' rename_tac [t |> dest_Var |> fst |> fst]
 
 fun release_quantifier_tac thy (skolem, t) =
-  (if skolem then fix_exists_tac else instantiate_forall_tac) thy t
+  (if skolem then fix_exists_tac else instantiate_forall_tac thy) t
 
 fun release_clusters_tac _ _ _ [] = K all_tac
   | release_clusters_tac thy ax_counts substs