1.1 --- a/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Sep 02 14:43:20 2011 +0200
     1.2 +++ b/src/HOL/Metis_Examples/Type_Encodings.thy	Fri Sep 02 14:43:20 2011 +0200
     1.3 @@ -70,7 +70,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_Tactics.metis_tac [type_enc] ctxt ths 1
     1.8 +               THEN Metis_Tactic.metis_tac [type_enc] 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