1.1 --- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
     1.2 +++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
     1.3 @@ -168,8 +168,7 @@
     1.4                    |> Metis_LiteralSet.fromList
     1.5                    |> Metis_Thm.axiom, isa)
     1.6      in
     1.7 -      if ident = type_tag_idempotence_helper_name orelse
     1.8 -         String.isPrefix tags_sym_formula_prefix ident then
     1.9 +      if String.isPrefix tags_sym_formula_prefix ident then
    1.10          Isa_Reflexive_or_Trivial |> some
    1.11        else if String.isPrefix conjecture_prefix ident then
    1.12          NONE