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 48131 1016664b8feb
parent 48130 defbcdc60fd6
child 48132 9aa0fad4e864 
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Tue Jun 26 11:14:39 2012 +0200
@@ -211,7 +211,7 @@
 fun prepare_metis_problem ctxt type_enc lam_trans conj_clauses fact_clauses =
   let
     val (conj_clauses, fact_clauses) =
-      if polymorphism_of_type_enc type_enc = Raw_Polymorphic then
+      if is_type_enc_polymorphic type_enc then
         (conj_clauses, fact_clauses)
       else
         conj_clauses @ fact_clauses
isabelle