# HG changeset patch
# User blanchet
# Date 1328565662 -3600
# Node ID 6f0f2b71fd69b7ac2253f66a5ecab3a6f9b0769c
# Parent  e9c90516bc0de846b5688b3d048bf10ec1ececa3
tuning

diff -r e9c90516bc0d -r 6f0f2b71fd69 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Feb 06 23:01:01 2012 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Mon Feb 06 23:01:02 2012 +0100
@@ -71,13 +71,13 @@
                     ATP_Problem_Generate.combsN ctxt ths 1
                THEN COND (has_fewer_prems 2) all_tac no_tac
                THEN tac type_encs)
-  in tac end
+  in tac type_encs end
 *}
 
 method_setup metis_exhaust = {*
   Attrib.thms >>
-    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths type_encs))
-*} "exhaustively run the new Metis with all type encodings"
+    (fn ths => fn ctxt => SIMPLE_METHOD (metis_exhaust_tac ctxt ths))
+*} "exhaustively run Metis with all type encodings"
 
 text {* Miscellaneous tests *}