src/HOL/Meson.thy
changeset 39950 f3c4849868b8
parent 39948 317010af8972
child 39953 aa54f347e5e2
--- a/src/HOL/Meson.thy	Tue Oct 05 10:30:50 2010 +0200
+++ b/src/HOL/Meson.thy	Tue Oct 05 10:59:12 2010 +0200
@@ -188,21 +188,12 @@
 
 section {* Meson package *}
 
-ML {*
-structure Meson_Choices = Named_Thms
-(
-  val name = "meson_choice"
-  val description = "choice axioms for MESON's (and Metis's) skolemizer"
-)
-*}
-
 use "Tools/Meson/meson.ML"
 use "Tools/Meson/meson_clausify.ML"
 use "Tools/Meson/meson_tactic.ML"
 
 setup {*
-  Meson_Choices.setup
-  #> Meson.setup
+  Meson.setup
   #> Meson_Tactic.setup
 *}