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/SMT2/smtlib2_isar.ML
changeset 57745 c65c116553b5
parent 57743 0af2d5dfb0ac
child 57748 31f5781fa9cd 
--- a/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/SMT2/smtlib2_isar.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -65,7 +65,6 @@
   |> not (null ll_defs) ? unlift_term ll_defs
   |> unskolemize_names
   |> HOLogic.mk_Trueprop
-  |> unskolemize_names
 
 fun normalizing_prems ctxt concl0 =
   SMT2_Normalize.case_bool_entry :: SMT2_Normalize.special_quant_table @
isabelle