tuning
authorblanchet
Mon, 06 Feb 2012 23:01:02 +0100
changeset 46436 6f0f2b71fd69
parent 46435 e9c90516bc0d
child 46437 9552b6f2c670
tuning
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 *}