# HG changeset patch
# User blanchet
# Date 1321460802 -3600
# Node ID 741f308c0f363ee91b57e68fd3e66129ad9d610f
# Parent  3b951bbd2beecb7aec82c65678f1318692388056
compile

diff -r 3b951bbd2bee -r 741f308c0f36 src/HOL/Metis_Examples/Type_Encodings.thy
--- a/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Nov 16 17:19:08 2011 +0100
+++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Wed Nov 16 17:26:42 2011 +0100
@@ -72,7 +72,7 @@
       | tac (type_enc :: type_encs) st =
         st (* |> tap (fn _ => tracing (PolyML.makestring type_enc)) *)
            |> ((if null type_encs then all_tac else rtac @{thm fork} 1)
-               THEN Metis_Tactic.metis_tac [type_enc] ctxt ths 1
+               THEN Metis_Tactic.metis_tac [type_enc] "combinators" ctxt ths 1
                THEN COND (has_fewer_prems 2) all_tac no_tac
                THEN tac type_encs)
   in tac end