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