--- 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 *}