Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Metis/metis_generate.ML
changeset 47046 62ca06cc5a99
parent 47039 1b36a05a070d
child 47912 12de57c5eee5 
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Mar 20 13:53:09 2012 +0100
@@ -168,8 +168,7 @@
                   |> Metis_LiteralSet.fromList
                   |> Metis_Thm.axiom, isa)
     in
-      if ident = type_tag_idempotence_helper_name orelse
-         String.isPrefix tags_sym_formula_prefix ident then
+      if String.isPrefix tags_sym_formula_prefix ident then
         Isa_Reflexive_or_Trivial |> some
       else if String.isPrefix conjecture_prefix ident then
         NONE
isabelle