# HG changeset patch
# User wenzelm
# Date 1279810380 -7200
# Node ID b8ca89c45086a8ff76c6d7d1bcf3a96a71da96eb
# Parent  d00a3f47b6072e9e07a6f6da261a4c15b419e6a7# Parent  f18c4bc8b02869584fe677d60a4adeee805a5bbb
merged

diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/IsaMakefile	Thu Jul 22 16:53:00 2010 +0200
@@ -424,7 +424,8 @@
   Library/Poly_Deriv.thy Library/Polynomial.thy				\
   Library/Predicate_Compile_Quickcheck.thy Library/Preorder.thy		\
   Library/Product_Vector.thy Library/Product_ord.thy			\
-  Library/Product_plus.thy Library/Quicksort.thy			\
+  Library/Product_plus.thy Library/Quickcheck_Types.thy 		\
+  Library/Quicksort.thy 						\
   Library/Quotient_List.thy Library/Quotient_Option.thy			\
   Library/Quotient_Product.thy Library/Quotient_Sum.thy			\
   Library/Quotient_Syntax.thy Library/Quotient_Type.thy			\
@@ -990,7 +991,8 @@
   ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy				\
   ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy			\
   ex/Multiquote.thy ex/NatSum.thy ex/Numeral.thy ex/PER.thy		\
-  ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy		\
+  ex/PresburgerEx.thy ex/Primrec.thy 					\
+  ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy 	\
   ex/ROOT.ML ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy		\
   ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
   ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy		\
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Library/Quickcheck_Types.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quickcheck_Types.thy	Thu Jul 22 16:53:00 2010 +0200
@@ -0,0 +1,467 @@
+(*  Title:      HOL/Library/Quickcheck_Types.thy
+    Author:     Lukas Bulwahn
+    Copyright   2010 TU Muenchen
+*)
+
+theory Quickcheck_Types
+imports Main
+begin
+
+text {*
+This theory provides some default types for the quickcheck execution.
+In most cases, the default type @{typ "int"} meets the sort constraints
+of the proposition.
+But for the type classes bot and top, the type @{typ "int"} is insufficient.
+Hence, we provide other types than @{typ "int"} as further default types.  
+*}
+
+subsection {* A non-distributive lattice *}
+
+datatype non_distrib_lattice = Zero | A | B | C | One
+
+instantiation non_distrib_lattice :: order
+begin
+
+definition less_eq_non_distrib_lattice
+where
+  "a <= b = (case a of Zero => True | A => (b = A) \<or> (b = One) | B => (b = B) \<or> (b = One) | C => (b = C) \<or> (b = One) | One => (b = One))"
+
+definition less_non_distrib_lattice
+where
+  "a < b = (case a of Zero => (b \<noteq> Zero) | A => (b = One) | B => (b = One) | C => (b = One) | One => False)"
+
+instance proof
+qed (auto simp add: less_eq_non_distrib_lattice_def less_non_distrib_lattice_def split: non_distrib_lattice.split non_distrib_lattice.split_asm)
+
+end
+
+instantiation non_distrib_lattice :: lattice
+begin
+
+
+definition sup_non_distrib_lattice
+where
+  "sup a b = (if a = b then a else (if a = Zero then b else (if b = Zero then a else One)))"
+
+definition inf_non_distrib_lattice
+where
+  "inf a b = (if a = b then a else (if a = One then b else (if b = One then a else Zero)))"
+
+instance proof
+qed (auto simp add: inf_non_distrib_lattice_def sup_non_distrib_lattice_def less_eq_non_distrib_lattice_def split: split_if non_distrib_lattice.split non_distrib_lattice.split_asm)
+
+end
+
+hide_const Zero A B C One
+
+subsection {* Values extended by a bottom element *}
+
+datatype 'a bot = Value 'a | Bot
+
+instantiation bot :: (preorder) preorder
+begin
+
+definition less_eq_bot where
+  "x \<le> y \<longleftrightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> x \<le> y))"
+
+definition less_bot where
+  "x < y \<longleftrightarrow> (case y of Bot \<Rightarrow> False | Value y \<Rightarrow> (case x of Bot \<Rightarrow> True | Value x \<Rightarrow> x < y))"
+
+lemma less_eq_bot_Bot [simp]: "Bot \<le> x"
+  by (simp add: less_eq_bot_def)
+
+lemma less_eq_bot_Bot_code [code]: "Bot \<le> x \<longleftrightarrow> True"
+  by simp
+
+lemma less_eq_bot_Bot_is_Bot: "x \<le> Bot \<Longrightarrow> x = Bot"
+  by (cases x) (simp_all add: less_eq_bot_def)
+
+lemma less_eq_bot_Value_Bot [simp, code]: "Value x \<le> Bot \<longleftrightarrow> False"
+  by (simp add: less_eq_bot_def)
+
+lemma less_eq_bot_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
+  by (simp add: less_eq_bot_def)
+
+lemma less_bot_Bot [simp, code]: "x < Bot \<longleftrightarrow> False"
+  by (simp add: less_bot_def)
+
+lemma less_bot_Bot_is_Value: "Bot < x \<Longrightarrow> \<exists>z. x = Value z"
+  by (cases x) (simp_all add: less_bot_def)
+
+lemma less_bot_Bot_Value [simp]: "Bot < Value x"
+  by (simp add: less_bot_def)
+
+lemma less_bot_Bot_Value_code [code]: "Bot < Value x \<longleftrightarrow> True"
+  by simp
+
+lemma less_bot_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
+  by (simp add: less_bot_def)
+
+instance proof
+qed (auto simp add: less_eq_bot_def less_bot_def less_le_not_le elim: order_trans split: bot.splits)
+
+end 
+
+instance bot :: (order) order proof
+qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+
+instance bot :: (linorder) linorder proof
+qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
+
+instantiation bot :: (preorder) bot
+begin
+
+definition "bot = Bot"
+
+instance proof
+qed (simp add: bot_bot_def)
+
+end
+
+instantiation bot :: (top) top
+begin
+
+definition "top = Value top"
+
+instance proof
+qed (simp add: top_bot_def less_eq_bot_def split: bot.split)
+
+end
+
+instantiation bot :: (semilattice_inf) semilattice_inf
+begin
+
+definition inf_bot
+where
+  "inf x y = (case x of Bot => Bot | Value v => (case y of Bot => Bot | Value v' => Value (inf v v')))"
+
+instance proof
+qed (auto simp add: inf_bot_def less_eq_bot_def split: bot.splits)
+
+end
+
+instantiation bot :: (semilattice_sup) semilattice_sup
+begin
+
+definition sup_bot
+where
+  "sup x y = (case x of Bot => y | Value v => (case y of Bot => x | Value v' => Value (sup v v')))"
+
+instance proof
+qed (auto simp add: sup_bot_def less_eq_bot_def split: bot.splits)
+
+end
+
+instance bot :: (lattice) bounded_lattice_bot ..
+
+section {* Values extended by a top element *}
+
+datatype 'a top = Value 'a | Top
+
+instantiation top :: (preorder) preorder
+begin
+
+definition less_eq_top where
+  "x \<le> y \<longleftrightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> x \<le> y))"
+
+definition less_top where
+  "x < y \<longleftrightarrow> (case x of Top \<Rightarrow> False | Value x \<Rightarrow> (case y of Top \<Rightarrow> True | Value y \<Rightarrow> x < y))"
+
+lemma less_eq_top_Top [simp]: "x <= Top"
+  by (simp add: less_eq_top_def)
+
+lemma less_eq_top_Top_code [code]: "x \<le> Top \<longleftrightarrow> True"
+  by simp
+
+lemma less_eq_top_is_Top: "Top \<le> x \<Longrightarrow> x = Top"
+  by (cases x) (simp_all add: less_eq_top_def)
+
+lemma less_eq_top_Top_Value [simp, code]: "Top \<le> Value x \<longleftrightarrow> False"
+  by (simp add: less_eq_top_def)
+
+lemma less_eq_top_Value_Value [simp, code]: "Value x \<le> Value y \<longleftrightarrow> x \<le> y"
+  by (simp add: less_eq_top_def)
+
+lemma less_top_Top [simp, code]: "Top < x \<longleftrightarrow> False"
+  by (simp add: less_top_def)
+
+lemma less_top_Top_is_Value: "x < Top \<Longrightarrow> \<exists>z. x = Value z"
+  by (cases x) (simp_all add: less_top_def)
+
+lemma less_top_Value_Top [simp]: "Value x < Top"
+  by (simp add: less_top_def)
+
+lemma less_top_Value_Top_code [code]: "Value x < Top \<longleftrightarrow> True"
+  by simp
+
+lemma less_top_Value [simp, code]: "Value x < Value y \<longleftrightarrow> x < y"
+  by (simp add: less_top_def)
+
+instance proof
+qed (auto simp add: less_eq_top_def less_top_def less_le_not_le elim: order_trans split: top.splits)
+
+end 
+
+instance top :: (order) order proof
+qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
+
+instance top :: (linorder) linorder proof
+qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
+
+instantiation top :: (preorder) top
+begin
+
+definition "top = Top"
+
+instance proof
+qed (simp add: top_top_def)
+
+end
+
+instantiation top :: (bot) bot
+begin
+
+definition "bot = Value bot"
+
+instance proof
+qed (simp add: bot_top_def less_eq_top_def split: top.split)
+
+end
+
+instantiation top :: (semilattice_inf) semilattice_inf
+begin
+
+definition inf_top
+where
+  "inf x y = (case x of Top => y | Value v => (case y of Top => x | Value v' => Value (inf v v')))"
+
+instance proof
+qed (auto simp add: inf_top_def less_eq_top_def split: top.splits)
+
+end
+
+instantiation top :: (semilattice_sup) semilattice_sup
+begin
+
+definition sup_top
+where
+  "sup x y = (case x of Top => Top | Value v => (case y of Top => Top | Value v' => Value (sup v v')))"
+
+instance proof
+qed (auto simp add: sup_top_def less_eq_top_def split: top.splits)
+
+end
+
+instance top :: (lattice) bounded_lattice_top ..
+
+
+datatype 'a flat_complete_lattice = Value 'a | Bot | Top
+
+instantiation flat_complete_lattice :: (type) order
+begin
+
+definition less_eq_flat_complete_lattice where
+  "x \<le> y == (case x of Bot => True | Value v1 => (case y of Bot => False | Value v2 => (v1 = v2) | Top => True) | Top => (y = Top))"
+
+definition less_flat_complete_lattice where
+  "x < y = (case x of Bot => \<not> (y = Bot) | Value v1 => (y = Top) | Top => False)"
+
+lemma [simp]: "Bot <= y"
+unfolding less_eq_flat_complete_lattice_def by auto
+
+lemma [simp]: "y <= Top"
+unfolding less_eq_flat_complete_lattice_def by (auto split: flat_complete_lattice.splits)
+
+lemma greater_than_two_values:
+  assumes "a ~= aa" "Value a <= z" "Value aa <= z"
+  shows "z = Top"
+using assms
+by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
+
+lemma lesser_than_two_values:
+  assumes "a ~= aa" "z <= Value a" "z <= Value aa"
+  shows "z = Bot"
+using assms
+by (cases z) (auto simp add: less_eq_flat_complete_lattice_def)
+
+instance proof
+qed (auto simp add: less_eq_flat_complete_lattice_def less_flat_complete_lattice_def split: flat_complete_lattice.splits)
+
+end
+
+instantiation flat_complete_lattice :: (type) bot
+begin
+
+definition "bot = Bot"
+
+instance proof
+qed (simp add: bot_flat_complete_lattice_def)
+
+end
+
+instantiation flat_complete_lattice :: (type) top
+begin
+
+definition "top = Top"
+
+instance proof
+qed (auto simp add: less_eq_flat_complete_lattice_def top_flat_complete_lattice_def split: flat_complete_lattice.splits)
+
+end
+
+instantiation flat_complete_lattice :: (type) lattice
+begin
+
+definition inf_flat_complete_lattice
+where
+  "inf x y = (case x of Bot => Bot | Value v1 => (case y of Bot => Bot | Value v2 => if (v1 = v2) then x else Bot | Top => x) | Top => y)"
+
+definition sup_flat_complete_lattice
+where
+  "sup x y = (case x of Bot => y | Value v1 => (case y of Bot => x | Value v2 => if v1 = v2 then x else Top | Top => Top) | Top => Top)"
+
+instance proof
+qed (auto simp add: inf_flat_complete_lattice_def sup_flat_complete_lattice_def less_eq_flat_complete_lattice_def split: flat_complete_lattice.splits)
+
+end
+
+instantiation flat_complete_lattice :: (type) complete_lattice
+begin
+
+definition Sup_flat_complete_lattice
+where
+  "Sup A = (if (A = {} \<or> A = {Bot}) then Bot else (if (\<exists> v. A - {Bot} = {Value v}) then Value (THE v. A - {Bot} = {Value v}) else Top))"
+
+definition Inf_flat_complete_lattice
+where
+  "Inf A = (if (A = {} \<or> A = {Top}) then Top else (if (\<exists> v. A - {Top} = {Value v}) then Value (THE v. A - {Top} = {Value v}) else Bot))"
+ 
+instance
+proof
+  fix x A
+  assume "(x :: 'a flat_complete_lattice) : A"
+  {
+    fix v
+    assume "A - {Top} = {Value v}"
+    from this have "(THE v. A - {Top} = {Value v}) = v"
+      by (auto intro!: the1_equality)
+    moreover
+    from `x : A` `A - {Top} = {Value v}` have "x = Top \<or> x = Value v"
+      by auto
+    ultimately have "Value (THE v. A - {Top} = {Value v}) <= x"
+      by auto
+  }
+  from `x : A` this show "Inf A <= x"
+    unfolding Inf_flat_complete_lattice_def
+    by fastsimp
+next
+  fix z A
+  assume z: "\<And>x. x : A ==> z <= (x :: 'a flat_complete_lattice)"
+  {
+    fix v
+    assume "A - {Top} = {Value v}"
+    moreover
+    from this have "(THE v. A - {Top} = {Value v}) = v"
+      by (auto intro!: the1_equality)
+    moreover
+    note z
+    moreover
+    ultimately have "z <= Value (THE v::'a. A - {Top} = {Value v})"
+      by auto
+  } moreover
+  {
+    assume not_one_value: "A ~= {}" "A ~= {Top}" "~ (EX v::'a. A - {Top} = {Value v})"
+    have "z <= Bot"
+    proof (cases "A - {Top} = {Bot}")
+      case True
+      from this z show ?thesis
+        by auto
+    next
+      case False
+      from not_one_value
+      obtain a1 where a1: "a1 : A - {Top}" by auto
+      from not_one_value False a1
+      obtain a2 where "a2 : A - {Top} \<and> a1 \<noteq> a2"
+        by (cases a1) auto
+      from this a1 z[of "a1"] z[of "a2"] show ?thesis
+        apply (cases a1)
+        apply auto
+        apply (cases a2)
+        apply auto
+        apply (auto dest!: lesser_than_two_values)
+        done
+    qed
+  } moreover
+  note z moreover
+  ultimately show "z <= Inf A"
+    unfolding Inf_flat_complete_lattice_def
+    by auto
+next
+  fix x A
+  assume "(x :: 'a flat_complete_lattice) : A"
+  {
+    fix v
+    assume "A - {Bot} = {Value v}"
+    from this have "(THE v. A - {Bot} = {Value v}) = v"
+      by (auto intro!: the1_equality)
+    moreover
+    from `x : A` `A - {Bot} = {Value v}` have "x = Bot \<or> x = Value v"
+      by auto
+    ultimately have "x <= Value (THE v. A - {Bot} = {Value v})"
+      by auto
+  }
+  from `x : A` this show "x <= Sup A"
+    unfolding Sup_flat_complete_lattice_def
+    by fastsimp
+next
+  fix z A
+  assume z: "\<And>x. x : A ==> x <= (z :: 'a flat_complete_lattice)"
+  {
+    fix v
+    assume "A - {Bot} = {Value v}"
+    moreover
+    from this have "(THE v. A - {Bot} = {Value v}) = v"
+      by (auto intro!: the1_equality)
+    moreover
+    note z
+    moreover
+    ultimately have "Value (THE v::'a. A - {Bot} = {Value v}) <= z"
+      by auto
+  } moreover
+  {
+    assume not_one_value: "A ~= {}" "A ~= {Bot}" "~ (EX v::'a. A - {Bot} = {Value v})"
+    have "Top <= z"
+    proof (cases "A - {Bot} = {Top}")
+      case True
+      from this z show ?thesis
+        by auto
+    next
+      case False
+      from not_one_value
+      obtain a1 where a1: "a1 : A - {Bot}" by auto
+      from not_one_value False a1
+      obtain a2 where "a2 : A - {Bot} \<and> a1 \<noteq> a2"
+        by (cases a1) auto
+      from this a1 z[of "a1"] z[of "a2"] show ?thesis
+        apply (cases a1)
+        apply auto
+        apply (cases a2)
+        apply (auto dest!: greater_than_two_values)
+        done
+    qed
+  } moreover
+  note z moreover
+  ultimately show "Sup A <= z"
+    unfolding Sup_flat_complete_lattice_def
+    by auto
+qed
+
+end
+
+section {* Quickcheck configuration *}
+
+quickcheck_params[default_type = ["int", "non_distrib_lattice", "int bot", "int top", "int flat_complete_lattice"]]
+
+hide_type non_distrib_lattice flat_complete_lattice bot top
+
+end
\ No newline at end of file
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Library/State_Monad.thy	Thu Jul 22 16:53:00 2010 +0200
@@ -5,7 +5,7 @@
 header {* Combinator syntax for generic, open state monads (single threaded monads) *}
 
 theory State_Monad
-imports Monad_Syntax
+imports Main Monad_Syntax
 begin
 
 subsection {* Motivation *}
@@ -113,10 +113,32 @@
 
 subsection {* Do-syntax *}
 
-setup {*
-  Adhoc_Overloading.add_variant @{const_name bind} @{const_name scomp}
-*}
+nonterminals
+  sdo_binds sdo_bind
+
+syntax
+  "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
+  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
+  "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
+  "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
+  "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
+  "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
 
+syntax (xsymbols)
+  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
+
+translations
+  "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
+    == "CONST scomp t (\<lambda>p. e)"
+  "_sdo_block (_sdo_cons (_sdo_then t) (_sdo_final e))"
+    == "CONST fcomp t e"
+  "_sdo_block (_sdo_cons (_sdo_let p t) bs)"
+    == "let p = t in _sdo_block bs"
+  "_sdo_block (_sdo_cons b (_sdo_cons c cs))"
+    == "_sdo_block (_sdo_cons b (_sdo_final (_sdo_block (_sdo_cons c cs))))"
+  "_sdo_cons (_sdo_let p t) (_sdo_final s)"
+    == "_sdo_final (let p = t in s)"
+  "_sdo_block (_sdo_final e)" => "e"
 
 text {*
   For an example, see HOL/Extraction/Higman.thy.
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -13,7 +13,7 @@
 fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
-    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
+    val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
   in
     (case TimeLimit.timeLimit timeout quickcheck pre of
       NONE => log (qc_tag id ^ "no counterexample")
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -9,7 +9,6 @@
 signature ATP_MANAGER =
 sig
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
-  type name_pool = Sledgehammer_TPTP_Format.name_pool
   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
   type params =
     {debug: bool,
@@ -38,7 +37,7 @@
   type prover_result =
     {outcome: failure option,
      message: string,
-     pool: name_pool option,
+     pool: string Symtab.table,
      relevant_thm_names: string list,
      atp_run_time_in_msecs: int,
      output: string,
@@ -108,7 +107,7 @@
 type prover_result =
   {outcome: failure option,
    message: string,
-   pool: name_pool option,
+   pool: string Symtab.table,
    relevant_thm_names: string list,
    atp_run_time_in_msecs: int,
    output: string,
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/ATP_Manager/atp_systems.ML
--- a/src/HOL/Tools/ATP_Manager/atp_systems.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_systems.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -19,7 +19,6 @@
 structure ATP_Systems : ATP_SYSTEMS =
 struct
 
-open Clausifier
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
@@ -133,14 +132,14 @@
 fun subtract_cls ax_clauses =
   filter_out (Termtab.defined (make_clause_table ax_clauses) o prop_of)
 
-fun is_false_literal (Literal (pos, CombConst ((c, _), _, _))) =
-      (pos andalso c = "c_False") orelse (not pos andalso c = "c_True")
+fun is_false_literal (FOLLiteral (pos, CombConst ((c, _), _, _))) =
+    c = (if pos then "c_False" else "c_True")
   | is_false_literal _ = false
-fun is_true_literal (Literal (pol, CombConst ((c, _), _, _))) =
+fun is_true_literal (FOLLiteral (pol, CombConst ((c, _), _, _))) =
       (pol andalso c = "c_True") orelse
       (not pol andalso c = "c_False")
   | is_true_literal _ = false;
-fun is_tautology (HOLClause {literals,...}) = exists is_true_literal literals
+fun is_tautology (FOLClause {literals,...}) = exists is_true_literal literals
 
 (* making axiom and conjecture clauses *)
 fun make_clause thy (clause_id, axiom_name, kind, th) skolems =
@@ -152,7 +151,7 @@
       raise TRIVIAL ()
     else
       (skolems,
-       HOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
+       FOLClause {clause_id = clause_id, axiom_name = axiom_name, th = th,
                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   end
 
@@ -180,12 +179,12 @@
     Symtab.map_entry c (Integer.add 1)
   | count_combterm (CombVar _) = I
   | count_combterm (CombApp (t1, t2)) = count_combterm t1 #> count_combterm t2
-fun count_literal (Literal (_, t)) = count_combterm t
-fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
+fun count_literal (FOLLiteral (_, t)) = count_combterm t
+fun count_clause (FOLClause {literals, ...}) = fold count_literal literals
 
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
-  #> (if raw then map (apfst (rpair 0)) else cnf_rules_pairs thy true)
+  #> (if raw then map (apfst (rpair 0)) else Clausifier.cnf_rules_pairs thy true)
 
 val optional_helpers =
   [(["c_COMBI", "c_COMBK"], (false, @{thms COMBI_def COMBK_def})),
@@ -233,10 +232,11 @@
     val helper_clauses =
       get_helper_clauses thy is_FO full_types conjectures extra_cls
     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
-    val classrel_clauses = make_classrel_clauses thy subs supers'
+    val class_rel_clauses = make_class_rel_clauses thy subs supers'
   in
     (Vector.fromList clnames,
-      (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
+      (conjectures, axiom_clauses, extra_clauses, helper_clauses,
+       class_rel_clauses, arity_clauses))
   end
 
 
@@ -255,7 +255,7 @@
     (* get clauses and prepare them for writing *)
     val (ctxt, (_, th)) = goal;
     val thy = ProofContext.theory_of ctxt;
-    val goal_clss = #1 (neg_conjecture_clauses ctxt th subgoal)
+    val goal_clss = #1 (Clausifier.neg_conjecture_clauses ctxt th subgoal)
     val goal_cls = List.concat goal_clss
     val the_filtered_clauses =
       case filtered_clauses of
@@ -264,7 +264,7 @@
                     relevance_convergence defs_relevant max_axiom_clauses
                     (the_default prefers_theory_relevant theory_relevant)
                     relevance_override goal goal_cls
-                |> cnf_rules_pairs thy true
+                |> Clausifier.cnf_rules_pairs thy true
     val the_axiom_clauses = axiom_clauses |> the_default the_filtered_clauses
     val (internal_thm_names, clauses) =
       prepare_clauses full_types goal_cls the_axiom_clauses the_filtered_clauses
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -492,7 +492,6 @@
           else
             0
         val settings = [("solver", commas_quote kodkod_sat_solver),
-                        ("skolem_depth", "-1"),
                         ("bit_width", string_of_int bit_width),
                         ("symmetry_breaking", "20"),
                         ("sharing", "3"),
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -547,59 +547,74 @@
                             skolem_depth =
   let
     val incrs = map (Integer.add 1)
-    fun aux ss Ts js depth polar t =
+    fun aux ss Ts js skolemizable polar t =
       let
         fun do_quantifier quant_s quant_T abs_s abs_T t =
-          if not (loose_bvar1 (t, 0)) then
-            aux ss Ts js depth polar (incr_boundvars ~1 t)
-          else if depth <= skolem_depth andalso
-                  is_positive_existential polar quant_s then
-            let
-              val j = length (!skolems) + 1
-              val sko_s = skolem_prefix_for (length js) j ^ abs_s
-              val _ = Unsynchronized.change skolems (cons (sko_s, ss))
-              val sko_t = list_comb (Const (sko_s, rev Ts ---> abs_T),
-                                     map Bound (rev js))
-              val abs_t = Abs (abs_s, abs_T, aux ss Ts (incrs js) depth polar t)
-            in
-              if null js then s_betapply Ts (abs_t, sko_t)
-              else Const (@{const_name Let}, abs_T --> quant_T) $ sko_t $ abs_t
-            end
-          else
-            Const (quant_s, quant_T)
-            $ Abs (abs_s, abs_T,
-                   if is_higher_order_type abs_T then
-                     t
+          (if not (loose_bvar1 (t, 0)) then
+             aux ss Ts js skolemizable polar (incr_boundvars ~1 t)
+           else if is_positive_existential polar quant_s then
+             let
+               val j = length (!skolems) + 1
+               val (js', (ss', Ts')) =
+                 js ~~ (ss ~~ Ts)
+                 |> filter (fn (j, _) => loose_bvar1 (t, j + 1))
+                 |> ListPair.unzip ||> ListPair.unzip
+             in
+               if skolemizable andalso length js' <= skolem_depth then
+                 let
+                   val sko_s = skolem_prefix_for (length js') j ^ abs_s
+                   val _ = Unsynchronized.change skolems (cons (sko_s, ss'))
+                   val sko_t = list_comb (Const (sko_s, rev Ts' ---> abs_T),
+                                          map Bound (rev js'))
+                   val abs_t = Abs (abs_s, abs_T,
+                                    aux ss Ts (incrs js) skolemizable polar t)
+                 in
+                   if null js' then
+                     s_betapply Ts (abs_t, sko_t)
                    else
-                     aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
-                         (depth + 1) polar t)
+                     Const (@{const_name Let}, abs_T --> quant_T) $ sko_t
+                     $ abs_t
+                 end
+               else
+                 raise SAME ()
+             end
+           else
+             raise SAME ())
+          handle SAME () =>
+                 Const (quant_s, quant_T)
+                 $ Abs (abs_s, abs_T,
+                        if is_higher_order_type abs_T then
+                          t
+                        else
+                          aux (abs_s :: ss) (abs_T :: Ts) (0 :: incrs js)
+                              skolemizable polar t)
       in
         case t of
           Const (s0 as @{const_name all}, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
         | @{const "==>"} $ t1 $ t2 =>
-          @{const "==>"} $ aux ss Ts js depth (flip_polarity polar) t1
-          $ aux ss Ts js depth polar t2
+          @{const "==>"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+          $ aux ss Ts js skolemizable polar t2
         | @{const Pure.conjunction} $ t1 $ t2 =>
-          @{const Pure.conjunction} $ aux ss Ts js depth polar t1
-          $ aux ss Ts js depth polar t2
+          @{const Pure.conjunction} $ aux ss Ts js skolemizable polar t1
+          $ aux ss Ts js skolemizable polar t2
         | @{const Trueprop} $ t1 =>
-          @{const Trueprop} $ aux ss Ts js depth polar t1
+          @{const Trueprop} $ aux ss Ts js skolemizable polar t1
         | @{const Not} $ t1 =>
-          @{const Not} $ aux ss Ts js depth (flip_polarity polar) t1
+          @{const Not} $ aux ss Ts js skolemizable (flip_polarity polar) t1
         | Const (s0 as @{const_name All}, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
         | Const (s0 as @{const_name Ex}, T0) $ Abs (s1, T1, t1) =>
           do_quantifier s0 T0 s1 T1 t1
         | @{const "op &"} $ t1 $ t2 =>
-          s_conj (pairself (aux ss Ts js depth polar) (t1, t2))
+          s_conj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
         | @{const "op |"} $ t1 $ t2 =>
-          s_disj (pairself (aux ss Ts js depth polar) (t1, t2))
+          s_disj (pairself (aux ss Ts js skolemizable polar) (t1, t2))
         | @{const "op -->"} $ t1 $ t2 =>
-          @{const "op -->"} $ aux ss Ts js depth (flip_polarity polar) t1
-          $ aux ss Ts js depth polar t2
+          @{const "op -->"} $ aux ss Ts js skolemizable (flip_polarity polar) t1
+          $ aux ss Ts js skolemizable polar t2
         | (t0 as Const (@{const_name Let}, _)) $ t1 $ t2 =>
-          t0 $ t1 $ aux ss Ts js depth polar t2
+          t0 $ t1 $ aux ss Ts js skolemizable polar t2
         | Const (x as (s, T)) =>
           if is_inductive_pred hol_ctxt x andalso
              not (is_well_founded_inductive_pred hol_ctxt x) then
@@ -609,7 +624,7 @@
                 if gfp then (lbfp_prefix, @{const "op |"})
                 else (ubfp_prefix, @{const "op &"})
               fun pos () = unrolled_inductive_pred_const hol_ctxt gfp x
-                           |> aux ss Ts js depth polar
+                           |> aux ss Ts js skolemizable polar
               fun neg () = Const (pref ^ s, T)
             in
               case polar |> gfp ? flip_polarity of
@@ -627,12 +642,13 @@
           else
             Const x
         | t1 $ t2 =>
-          s_betapply Ts (aux ss Ts [] (skolem_depth + 1) polar t1,
-                         aux ss Ts [] depth Neut t2)
-        | Abs (s, T, t1) => Abs (s, T, aux ss Ts (incrs js) depth polar t1)
+          s_betapply Ts (aux ss Ts [] false polar t1,
+                         aux ss Ts [] skolemizable Neut t2)
+        | Abs (s, T, t1) =>
+          Abs (s, T, aux ss Ts (incrs js) skolemizable polar t1)
         | _ => t
       end
-  in aux [] [] [] 0 Pos end
+  in aux [] [] [] true Pos end
 
 (** Function specialization **)
 
@@ -1216,7 +1232,7 @@
 
 (** Preprocessor entry point **)
 
-val max_skolem_depth = 4
+val max_skolem_depth = 3
 
 fun preprocess_term (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs,
                                   boxes, ...}) finitizes monos t =
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -114,7 +114,8 @@
     end
   else
     case (fst (strip_comb atom)) of
-      (Const (@{const_name If}, _)) => let
+      (Const (@{const_name If}, _)) =>
+        let
           val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
           val atom' = MetaSimplifier.rewrite_term thy
             (map (fn th => th RS @{thm eq_reflection}) [@{thm if_bool_eq_disj}, if_beta]) [] atom
@@ -193,9 +194,10 @@
     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
+    val ctxt'' = ProofContext.transfer thy' ctxt'
     val tac = fn _ => Skip_Proof.cheat_tac thy'
-    val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
-      |> Variable.export ctxt' ctxt
+    val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros'
+      |> Variable.export ctxt'' ctxt
   in
     (intros'', (local_defs, thy'))
   end
@@ -287,6 +289,9 @@
         else
           error ("unexpected specification for constant " ^ quote constname ^ ":\n"
             ^ commas (map (quote o Display.string_of_thm_global thy) specs))
+      val if_beta = @{lemma "(if c then x else y) z = (if c then x z else y z)" by simp}
+      val intros = map (MetaSimplifier.rewrite_rule
+          [if_beta RS @{thm eq_reflection}]) intros
       val _ = print_specs options thy "normalized intros" intros
       (*val intros = maps (split_cases thy) intros*)
       val (intros', (local_defs, thy')) = flatten_intros constname intros thy
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/metis_clauses.ML
--- a/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_clauses.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -18,20 +18,20 @@
     TVarLit of name * name
   datatype arity_clause = ArityClause of
    {axiom_name: string, conclLit: arLit, premLits: arLit list}
-  datatype classrel_clause = ClassrelClause of
+  datatype class_rel_clause = ClassRelClause of
    {axiom_name: string, subclass: name, superclass: name}
   datatype combtyp =
-    TyVar of name |
-    TyFree of name |
-    TyConstr of name * combtyp list
+    CombTVar of name |
+    CombTFree of name |
+    CombType of name * combtyp list
   datatype combterm =
     CombConst of name * combtyp * combtyp list (* Const and Free *) |
     CombVar of name * combtyp |
     CombApp of combterm * combterm
-  datatype literal = Literal of bool * combterm
-  datatype hol_clause =
-    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                  literals: literal list, ctypes_sorts: typ list}
+  datatype fol_literal = FOLLiteral of bool * combterm
+  datatype fol_clause =
+    FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+                  literals: fol_literal list, ctypes_sorts: typ list}
 
   val type_wrapper_name : string
   val schematic_var_prefix: string
@@ -59,11 +59,11 @@
   val is_skolem_const_name: string -> bool
   val num_type_args: theory -> string -> int
   val type_literals_for_types : typ list -> type_literal list
-  val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
+  val make_class_rel_clauses: theory -> class list -> class list -> class_rel_clause list
   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   val type_of_combterm : combterm -> combtyp
   val strip_combterm_comb : combterm -> combterm * combterm list
-  val literals_of_term : theory -> term -> literal list * typ list
+  val literals_of_term : theory -> term -> fol_literal list * typ list
   val conceal_skolem_terms :
     int -> (string * term) list -> term -> (string * term) list * term
   val reveal_skolem_terms : (string * term) list -> term -> term
@@ -75,8 +75,6 @@
 structure Metis_Clauses : METIS_CLAUSES =
 struct
 
-open Clausifier
-
 val type_wrapper_name = "ti"
 
 val schematic_var_prefix = "V_";
@@ -85,7 +83,7 @@
 val tvar_prefix = "T_";
 val tfree_prefix = "t_";
 
-val classrel_clause_prefix = "clsrel_";
+val class_rel_clause_prefix = "clsrel_";
 
 val const_prefix = "c_";
 val type_const_prefix = "tc_";
@@ -288,8 +286,8 @@
 
 (**** Isabelle class relations ****)
 
-datatype classrel_clause =
-  ClassrelClause of {axiom_name: string, subclass: name, superclass: name}
+datatype class_rel_clause =
+  ClassRelClause of {axiom_name: string, subclass: name, superclass: name}
 
 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
 fun class_pairs _ [] _ = []
@@ -300,14 +298,14 @@
         fun add_supers sub = fold (add_super sub) supers
       in fold add_supers subs [] end
 
-fun make_classrel_clause (sub,super) =
-  ClassrelClause {axiom_name = classrel_clause_prefix ^ ascii_of sub ^ "_" ^
+fun make_class_rel_clause (sub,super) =
+  ClassRelClause {axiom_name = class_rel_clause_prefix ^ ascii_of sub ^ "_" ^
                                ascii_of super,
                   subclass = `make_type_class sub,
                   superclass = `make_type_class super};
 
-fun make_classrel_clauses thy subs supers =
-  map make_classrel_clause (class_pairs thy subs supers);
+fun make_class_rel_clauses thy subs supers =
+  map make_class_rel_clause (class_pairs thy subs supers);
 
 
 (** Isabelle arities **)
@@ -352,27 +350,27 @@
   in  (classes', multi_arity_clause cpairs)  end;
 
 datatype combtyp =
-  TyVar of name |
-  TyFree of name |
-  TyConstr of name * combtyp list
+  CombTVar of name |
+  CombTFree of name |
+  CombType of name * combtyp list
 
 datatype combterm =
   CombConst of name * combtyp * combtyp list (* Const and Free *) |
   CombVar of name * combtyp |
   CombApp of combterm * combterm
 
-datatype literal = Literal of bool * combterm
+datatype fol_literal = FOLLiteral of bool * combterm
 
-datatype hol_clause =
-  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
-                literals: literal list, ctypes_sorts: typ list}
+datatype fol_clause =
+  FOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+                literals: fol_literal list, ctypes_sorts: typ list}
 
 (*********************************************************************)
 (* convert a clause with type Term.term to a clause with type clause *)
 (*********************************************************************)
 
 (*Result of a function type; no need to check that the argument type matches.*)
-fun result_type (TyConstr (_, [_, tp2])) = tp2
+fun result_type (CombType (_, [_, tp2])) = tp2
   | result_type _ = raise Fail "non-function type"
 
 fun type_of_combterm (CombConst (_, tp, _)) = tp
@@ -387,11 +385,11 @@
 
 fun type_of (Type (a, Ts)) =
     let val (folTypes,ts) = types_of Ts in
-      (TyConstr (`make_fixed_type_const a, folTypes), ts)
+      (CombType (`make_fixed_type_const a, folTypes), ts)
     end
-  | type_of (tp as TFree (a, _)) = (TyFree (`make_fixed_type_var a), [tp])
+  | type_of (tp as TFree (a, _)) = (CombTFree (`make_fixed_type_var a), [tp])
   | type_of (tp as TVar (x, _)) =
-    (TyVar (make_schematic_type_var x, string_of_indexname x), [tp])
+    (CombTVar (make_schematic_type_var x, string_of_indexname x), [tp])
 and types_of Ts =
     let val (folTyps, ts) = ListPair.unzip (map type_of Ts) in
       (folTyps, union_all ts)
@@ -399,10 +397,10 @@
 
 (* same as above, but no gathering of sort information *)
 fun simp_type_of (Type (a, Ts)) =
-      TyConstr (`make_fixed_type_const a, map simp_type_of Ts)
-  | simp_type_of (TFree (a, _)) = TyFree (`make_fixed_type_var a)
+      CombType (`make_fixed_type_const a, map simp_type_of Ts)
+  | simp_type_of (TFree (a, _)) = CombTFree (`make_fixed_type_var a)
   | simp_type_of (TVar (x, _)) =
-    TyVar (make_schematic_type_var x, string_of_indexname x)
+    CombTVar (make_schematic_type_var x, string_of_indexname x)
 
 (* convert a Term.term (with combinators) into a combterm, also accummulate sort info *)
 fun combterm_of thy (Const (c, T)) =
@@ -439,7 +437,7 @@
     literals_of_term1 (literals_of_term1 args thy P) thy Q
   | literals_of_term1 (lits, ts) thy P =
     let val ((pred, ts'), pol) = predicate_of thy (P, true) in
-      (Literal (pol, pred) :: lits, union (op =) ts ts')
+      (FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
     end
 val literals_of_term = literals_of_term1 ([], [])
 
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -18,7 +18,6 @@
 structure Metis_Tactics : METIS_TACTICS =
 struct
 
-open Clausifier
 open Metis_Clauses
 
 exception METIS of string * string
@@ -70,10 +69,10 @@
 
 fun metis_lit b c args = (b, (c, args));
 
-fun hol_type_to_fol (TyVar (x, _)) = Metis.Term.Var x
-  | hol_type_to_fol (TyFree (s, _)) = Metis.Term.Fn (s, [])
-  | hol_type_to_fol (TyConstr ((s, _), tps)) =
-    Metis.Term.Fn (s, map hol_type_to_fol tps);
+fun metis_term_from_combtyp (CombTVar (s, _)) = Metis.Term.Var s
+  | metis_term_from_combtyp (CombTFree (s, _)) = Metis.Term.Fn (s, [])
+  | metis_term_from_combtyp (CombType ((s, _), tps)) =
+    Metis.Term.Fn (s, map metis_term_from_combtyp tps);
 
 (*These two functions insert type literals before the real literals. That is the
   opposite order from TPTP linkup, but maybe OK.*)
@@ -81,7 +80,7 @@
 fun hol_term_to_fol_FO tm =
   case strip_combterm_comb tm of
       (CombConst ((c, _), _, tys), tms) =>
-        let val tyargs = map hol_type_to_fol tys
+        let val tyargs = map metis_term_from_combtyp tys
             val args   = map hol_term_to_fol_FO tms
         in Metis.Term.Fn (c, tyargs @ args) end
     | (CombVar ((v, _), _), []) => Metis.Term.Var v
@@ -89,12 +88,12 @@
 
 fun hol_term_to_fol_HO (CombVar ((s, _), _)) = Metis.Term.Var s
   | hol_term_to_fol_HO (CombConst ((a, _), _, tylist)) =
-      Metis.Term.Fn (fn_isa_to_met a, map hol_type_to_fol tylist)
+      Metis.Term.Fn (fn_isa_to_met a, map metis_term_from_combtyp tylist)
   | hol_term_to_fol_HO (CombApp (tm1, tm2)) =
        Metis.Term.Fn (".", map hol_term_to_fol_HO [tm1, tm2]);
 
 (*The fully-typed translation, to avoid type errors*)
-fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, hol_type_to_fol ty]);
+fun wrap_type (tm, ty) = Metis.Term.Fn("ti", [tm, metis_term_from_combtyp ty]);
 
 fun hol_term_to_fol_FT (CombVar ((s, _), ty)) = wrap_type (Metis.Term.Var s, ty)
   | hol_term_to_fol_FT (CombConst((a, _), ty, _)) =
@@ -103,21 +102,21 @@
        wrap_type (Metis.Term.Fn(".", map hol_term_to_fol_FT [tm1,tm2]),
                   type_of_combterm tm);
 
-fun hol_literal_to_fol FO (Literal (pol, tm)) =
+fun hol_literal_to_fol FO (FOLLiteral (pos, tm)) =
       let val (CombConst((p, _), _, tys), tms) = strip_combterm_comb tm
-          val tylits = if p = "equal" then [] else map hol_type_to_fol tys
+          val tylits = if p = "equal" then [] else map metis_term_from_combtyp tys
           val lits = map hol_term_to_fol_FO tms
-      in metis_lit pol (fn_isa_to_met p) (tylits @ lits) end
-  | hol_literal_to_fol HO (Literal (pol, tm)) =
+      in metis_lit pos (fn_isa_to_met p) (tylits @ lits) end
+  | hol_literal_to_fol HO (FOLLiteral (pos, tm)) =
      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
-            metis_lit pol "=" (map hol_term_to_fol_HO tms)
-        | _ => metis_lit pol "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
-  | hol_literal_to_fol FT (Literal (pol, tm)) =
+            metis_lit pos "=" (map hol_term_to_fol_HO tms)
+        | _ => metis_lit pos "{}" [hol_term_to_fol_HO tm])   (*hBOOL*)
+  | hol_literal_to_fol FT (FOLLiteral (pos, tm)) =
      (case strip_combterm_comb tm of
           (CombConst(("equal", _), _, _), tms) =>
-            metis_lit pol "=" (map hol_term_to_fol_FT tms)
-        | _ => metis_lit pol "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
+            metis_lit pos "=" (map hol_term_to_fol_FT tms)
+        | _ => metis_lit pos "{}" [hol_term_to_fol_FT tm])   (*hBOOL*);
 
 fun literals_of_hol_term thy mode t =
       let val (lits, types_sorts) = literals_of_term thy t
@@ -170,11 +169,11 @@
 
 (* CLASSREL CLAUSE *)
 
-fun m_classrel_cls (subclass, _) (superclass, _) =
+fun m_class_rel_cls (subclass, _) (superclass, _) =
   [metis_lit false subclass [Metis.Term.Var "T"], metis_lit true superclass [Metis.Term.Var "T"]];
 
-fun classrel_cls (ClassrelClause {subclass, superclass, ...}) =
-  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_classrel_cls subclass superclass)));
+fun class_rel_cls (ClassRelClause {subclass, superclass, ...}) =
+  (TrueI, Metis.Thm.axiom (Metis.LiteralSet.fromList (m_class_rel_cls subclass superclass)));
 
 (* ------------------------------------------------------------------------- *)
 (* FOL to HOL  (Metis to Isabelle)                                           *)
@@ -223,22 +222,23 @@
 
 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
 
-fun fol_type_to_isa _ (Metis.Term.Var v) =
+fun hol_type_from_metis_term _ (Metis.Term.Var v) =
      (case strip_prefix tvar_prefix v of
           SOME w => make_tvar w
         | NONE   => make_tvar v)
-  | fol_type_to_isa ctxt (Metis.Term.Fn(x, tys)) =
+  | hol_type_from_metis_term ctxt (Metis.Term.Fn(x, tys)) =
      (case strip_prefix type_const_prefix x of
-          SOME tc => Term.Type (invert_const tc, map (fol_type_to_isa ctxt) tys)
+          SOME tc => Term.Type (invert_const tc,
+                                map (hol_type_from_metis_term ctxt) tys)
         | NONE    =>
       case strip_prefix tfree_prefix x of
           SOME tf => mk_tfree ctxt tf
-        | NONE    => raise Fail ("fol_type_to_isa: " ^ x));
+        | NONE    => raise Fail ("hol_type_from_metis_term: " ^ x));
 
 (*Maps metis terms to isabelle terms*)
-fun hol_term_from_fol_PT ctxt fol_tm =
+fun hol_term_from_metis_PT ctxt fol_tm =
   let val thy = ProofContext.theory_of ctxt
-      val _ = trace_msg (fn () => "hol_term_from_fol_PT: " ^
+      val _ = trace_msg (fn () => "hol_term_from_metis_PT: " ^
                                   Metis.Term.toString fol_tm)
       fun tm_to_tt (Metis.Term.Var v) =
              (case strip_prefix tvar_prefix v of
@@ -298,8 +298,8 @@
   end
 
 (*Maps fully-typed metis terms to isabelle terms*)
-fun hol_term_from_fol_FT ctxt fol_tm =
-  let val _ = trace_msg (fn () => "hol_term_from_fol_FT: " ^
+fun hol_term_from_metis_FT ctxt fol_tm =
+  let val _ = trace_msg (fn () => "hol_term_from_metis_FT: " ^
                                   Metis.Term.toString fol_tm)
       fun cvt (Metis.Term.Fn ("ti", [Metis.Term.Var v, _])) =
              (case strip_prefix schematic_var_prefix v of
@@ -312,8 +312,8 @@
                 SOME c => Const (invert_const c, dummyT)
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix fixed_var_prefix x of
-                SOME v => Free (v, fol_type_to_isa ctxt ty)
-              | NONE => raise Fail ("hol_term_from_fol_FT bad constant: " ^ x))
+                SOME v => Free (v, hol_type_from_metis_term ctxt ty)
+              | NONE => raise Fail ("hol_term_from_metis_FT bad constant: " ^ x))
         | cvt (Metis.Term.Fn ("ti", [Metis.Term.Fn (".",[tm1,tm2]), _])) =
             cvt tm1 $ cvt tm2
         | cvt (Metis.Term.Fn (".",[tm1,tm2])) = (*untyped application*)
@@ -327,17 +327,17 @@
               | NONE => (*Not a constant. Is it a fixed variable??*)
             case strip_prefix fixed_var_prefix x of
                 SOME v => Free (v, dummyT)
-              | NONE => (trace_msg (fn () => "hol_term_from_fol_FT bad const: " ^ x);
-                  hol_term_from_fol_PT ctxt t))
-        | cvt t = (trace_msg (fn () => "hol_term_from_fol_FT bad term: " ^ Metis.Term.toString t);
-            hol_term_from_fol_PT ctxt t)
+              | NONE => (trace_msg (fn () => "hol_term_from_metis_FT bad const: " ^ x);
+                  hol_term_from_metis_PT ctxt t))
+        | cvt t = (trace_msg (fn () => "hol_term_from_metis_FT bad term: " ^ Metis.Term.toString t);
+            hol_term_from_metis_PT ctxt t)
   in fol_tm |> cvt end
 
-fun hol_term_from_fol FT = hol_term_from_fol_FT
-  | hol_term_from_fol _ = hol_term_from_fol_PT
+fun hol_term_from_metis FT = hol_term_from_metis_FT
+  | hol_term_from_metis _ = hol_term_from_metis_PT
 
 fun hol_terms_from_fol ctxt mode skolems fol_tms =
-  let val ts = map (hol_term_from_fol mode ctxt) fol_tms
+  let val ts = map (hol_term_from_metis mode ctxt) fol_tms
       val _ = trace_msg (fn () => "  calling type inference:")
       val _ = app (fn t => trace_msg (fn () => Syntax.string_of_term ctxt t)) ts
       val ts' = ts |> map (reveal_skolem_terms skolems) |> infer_types ctxt
@@ -398,7 +398,7 @@
       fun subst_translation (x,y) =
             let val v = find_var x
                 (* We call "reveal_skolem_terms" and "infer_types" below. *)
-                val t = hol_term_from_fol mode ctxt y
+                val t = hol_term_from_metis mode ctxt y
             in  SOME (cterm_of thy (Var v), t)  end
             handle Option =>
                 (trace_msg (fn() => "List.find failed for the variable " ^ x ^
@@ -599,15 +599,15 @@
 (* ------------------------------------------------------------------------- *)
 
 fun cnf_helper_theorem thy raw th =
-  if raw then th else the_single (cnf_axiom thy false th)
+  if raw then th else the_single (Clausifier.cnf_axiom thy false th)
 
 fun type_ext thy tms =
   let val subs = tfree_classes_of_terms tms
       val supers = tvar_classes_of_terms tms
       and tycons = type_consts_of_terms thy tms
       val (supers', arity_clauses) = make_arity_clauses thy tycons supers
-      val classrel_clauses = make_classrel_clauses thy subs supers'
-  in  map classrel_cls classrel_clauses @ map arity_cls arity_clauses
+      val class_rel_clauses = make_class_rel_clauses thy subs supers'
+  in  map class_rel_cls class_rel_clauses @ map arity_cls arity_clauses
   end;
 
 (* ------------------------------------------------------------------------- *)
@@ -715,7 +715,7 @@
 fun FOL_SOLVE mode ctxt cls ths0 =
   let val thy = ProofContext.theory_of ctxt
       val th_cls_pairs =
-        map (fn th => (Thm.get_name_hint th, cnf_axiom thy false th)) ths0
+        map (fn th => (Thm.get_name_hint th, Clausifier.cnf_axiom thy false th)) ths0
       val ths = maps #2 th_cls_pairs
       val _ = trace_msg (fn () => "FOL_SOLVE: CONJECTURE CLAUSES")
       val _ = app (fn th => trace_msg (fn () => Display.string_of_thm ctxt th)) cls
@@ -774,15 +774,16 @@
   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
 
 fun generic_metis_tac mode ctxt ths i st0 =
-  let val _ = trace_msg (fn () =>
+  let
+    val _ = trace_msg (fn () =>
         "Metis called with theorems " ^ cat_lines (map (Display.string_of_thm ctxt) ths))
   in
     if exists_type type_has_top_sort (prop_of st0) then
       (warning ("Metis: Proof state contains the universal sort {}"); Seq.empty)
     else
-      (Meson.MESON (maps neg_clausify)
-                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
-                   ctxt i) st0
+      Meson.MESON (maps Clausifier.neg_clausify)
+                  (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
+                  ctxt i st0
      handle ERROR msg => raise METIS ("generic_metis_tac", msg)
   end
   handle METIS (loc, msg) =>
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -18,7 +18,6 @@
 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
 struct
 
-open Clausifier
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Proof_Reconstruct
@@ -56,7 +55,7 @@
     val _ = priority ("Testing " ^ string_of_int num_theorems ^
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
-    val axclauses = cnf_rules_pairs thy true name_thm_pairs
+    val axclauses = Clausifier.cnf_rules_pairs thy true name_thm_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -17,7 +17,6 @@
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
-open Clausifier
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
 open ATP_Manager
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -8,18 +8,17 @@
 signature SLEDGEHAMMER_PROOF_RECONSTRUCT =
 sig
   type minimize_command = string list -> string
-  type name_pool = Sledgehammer_TPTP_Format.name_pool
 
   val metis_line: bool -> int -> int -> string list -> string
   val metis_proof_text:
     bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val isar_proof_text:
-    name_pool option * bool * int * Proof.context * int list list
+    string Symtab.table * bool * int * Proof.context * int list list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
   val proof_text:
-    bool -> name_pool option * bool * int * Proof.context * int list list
+    bool -> string Symtab.table * bool * int * Proof.context * int list list
     -> bool * minimize_command * string * string vector * thm * int
     -> string * string list
 end;
@@ -27,7 +26,6 @@
 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
 struct
 
-open Clausifier
 open Metis_Clauses
 open Sledgehammer_Util
 open Sledgehammer_Fact_Filter
@@ -44,12 +42,6 @@
 fun is_conjecture_clause_number conjecture_shape num =
   index_in_shape num conjecture_shape >= 0
 
-fun ugly_name NONE s = s
-  | ugly_name (SOME the_pool) s =
-    case Symtab.lookup (snd the_pool) s of
-      SOME s' => s'
-    | NONE => s
-
 fun smart_lambda v t =
   Abs (case v of
          Const (s, _) =>
@@ -104,7 +96,7 @@
   | repair_name _ "$false" = "c_False"
   | repair_name _ "$$e" = "c_equal" (* seen in Vampire 11 proofs *)
   | repair_name _ "equal" = "c_equal" (* probably not needed *)
-  | repair_name pool s = ugly_name pool s
+  | repair_name pool s = Symtab.lookup pool s |> the_default s
 (* Generalized first-order terms, which include file names, numbers, etc. *)
 (* The "x" argument is not strictly necessary, but without it Poly/ML loops
    forever at compile time. *)
@@ -144,12 +136,12 @@
 fun ints_of_node (IntLeaf n) = cons n
   | ints_of_node (StrNode (_, us)) = fold ints_of_node us
 val parse_tstp_annotations =
-  Scan.optional ($$ "," |-- parse_term NONE
-                   --| Scan.option ($$ "," |-- parse_terms NONE)
+  Scan.optional ($$ "," |-- parse_term Symtab.empty
+                   --| Scan.option ($$ "," |-- parse_terms Symtab.empty)
                  >> (fn source => ints_of_node source [])) []
 
 fun parse_definition pool =
-  $$ "(" |-- parse_literal NONE --| Scan.this_string "<=>"
+  $$ "(" |-- parse_literal pool --| Scan.this_string "<=>"
   -- parse_clause pool --| $$ ")"
 
 (* Syntax: cnf(<num>, <formula_role>, <cnf_formula> <annotations>).
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tptp_format.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -7,16 +7,15 @@
 
 signature SLEDGEHAMMER_TPTP_FORMAT =
 sig
-  type classrel_clause = Metis_Clauses.classrel_clause
+  type class_rel_clause = Metis_Clauses.class_rel_clause
   type arity_clause = Metis_Clauses.arity_clause
-  type hol_clause = Metis_Clauses.hol_clause
-  type name_pool = string Symtab.table * string Symtab.table
+  type fol_clause = Metis_Clauses.fol_clause
 
   val write_tptp_file :
     theory -> bool -> bool -> bool -> Path.T
-    -> hol_clause list * hol_clause list * hol_clause list * hol_clause list
-       * classrel_clause list * arity_clause list
-    -> name_pool option * int
+    -> fol_clause list * fol_clause list * fol_clause list * fol_clause list
+       * class_rel_clause list * arity_clause list
+    -> string Symtab.table * int
 end;
 
 structure Sledgehammer_TPTP_Format : SLEDGEHAMMER_TPTP_FORMAT =
@@ -56,8 +55,6 @@
 
 (** Nice names **)
 
-type name_pool = string Symtab.table * string Symtab.table
-
 fun empty_name_pool readable_names =
   if readable_names then SOME (Symtab.empty, Symtab.empty) else NONE
 
@@ -105,9 +102,9 @@
 fun nice_atp_literal (pos, t) = nice_atp_term t #>> pair pos
 fun nice_problem_line (Cnf (ident, kind, lits)) =
   pool_map nice_atp_literal lits #>> (fn lits => Cnf (ident, kind, lits))
-val nice_problem =
+fun nice_problem problem =
   pool_map (fn (heading, lines) =>
-               pool_map nice_problem_line lines #>> pair heading)
+               pool_map nice_problem_line lines #>> pair heading) problem
 
 
 (** Sledgehammer stuff **)
@@ -120,9 +117,9 @@
 
 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
 
-fun atp_term_for_combtyp (TyVar name) = ATerm (name, [])
-  | atp_term_for_combtyp (TyFree name) = ATerm (name, [])
-  | atp_term_for_combtyp (TyConstr (name, tys)) =
+fun atp_term_for_combtyp (CombTVar name) = ATerm (name, [])
+  | atp_term_for_combtyp (CombTFree name) = ATerm (name, [])
+  | atp_term_for_combtyp (CombType (name, tys)) =
     ATerm (name, map atp_term_for_combtyp tys)
 
 fun atp_term_for_combterm full_types top_level u =
@@ -145,7 +142,7 @@
     else t
   end
 
-fun atp_literal_for_literal full_types (Literal (pos, t)) =
+fun atp_literal_for_literal full_types (FOLLiteral (pos, t)) =
   (pos, atp_term_for_combterm full_types true t)
 
 fun atp_literal_for_type_literal pos (TyLitVar (class, name)) =
@@ -154,18 +151,18 @@
     (pos, ATerm (class, [ATerm (name, [])]))
 
 fun atp_literals_for_axiom full_types
-        (HOLClause {literals, ctypes_sorts, ...}) =
+                           (FOLClause {literals, ctypes_sorts, ...}) =
   map (atp_literal_for_literal full_types) literals @
   map (atp_literal_for_type_literal false)
       (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_axiom full_types
-        (clause as HOLClause {axiom_name, clause_id, kind, ...}) =
+        (clause as FOLClause {axiom_name, clause_id, kind, ...}) =
   Cnf (hol_ident axiom_name clause_id, kind,
        atp_literals_for_axiom full_types clause)
 
-fun problem_line_for_classrel
-        (ClassrelClause {axiom_name, subclass, superclass, ...}) =
+fun problem_line_for_class_rel_clause
+        (ClassRelClause {axiom_name, subclass, superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
     Cnf (ascii_of axiom_name, Axiom, [(false, ATerm (subclass, [ty_arg])),
                                       (true, ATerm (superclass, [ty_arg]))])
@@ -176,16 +173,17 @@
   | atp_literal_for_arity_literal (TVarLit (c, sort)) =
     (false, ATerm (c, [ATerm (sort, [])]))
 
-fun problem_line_for_arity (ArityClause {axiom_name, conclLit, premLits, ...}) =
+fun problem_line_for_arity_clause
+        (ArityClause {axiom_name, conclLit, premLits, ...}) =
   Cnf (arity_clause_prefix ^ ascii_of axiom_name, Axiom,
        map atp_literal_for_arity_literal (conclLit :: premLits))
 
 fun problem_line_for_conjecture full_types
-        (clause as HOLClause {axiom_name, clause_id, kind, literals, ...}) =
+        (clause as FOLClause {axiom_name, clause_id, kind, literals, ...}) =
   Cnf (hol_ident axiom_name clause_id, kind,
        map (atp_literal_for_literal full_types) literals)
 
-fun atp_free_type_literals_for_conjecture (HOLClause {ctypes_sorts, ...}) =
+fun atp_free_type_literals_for_conjecture (FOLClause {ctypes_sorts, ...}) =
   map (atp_literal_for_type_literal true) (type_literals_for_types ctypes_sorts)
 
 fun problem_line_for_free_type lit = Cnf ("tfree_tcs", Conjecture, [lit])
@@ -216,7 +214,7 @@
   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
 fun consider_literal (_, t) = consider_term true t
 fun consider_problem_line (Cnf (_, _, lits)) = fold consider_literal lits
-val consider_problem = fold (fold consider_problem_line o snd)
+fun consider_problem problem = fold (fold consider_problem_line o snd) problem
 
 fun const_table_for_problem explicit_apply problem =
   if explicit_apply then NONE
@@ -295,25 +293,26 @@
           |> repair_predicates_in_term const_tab)
 fun repair_problem_line thy full_types const_tab (Cnf (ident, kind, lits)) =
   Cnf (ident, kind, map (repair_literal thy full_types const_tab) lits)
-val repair_problem_with_const_table = map o apsnd o map ooo repair_problem_line
-
+fun repair_problem_with_const_table thy full_types const_tab problem =
+  map (apsnd (map (repair_problem_line thy full_types const_tab))) problem
 fun repair_problem thy full_types explicit_apply problem =
   repair_problem_with_const_table thy full_types
       (const_table_for_problem explicit_apply problem) problem
 
 fun write_tptp_file thy readable_names full_types explicit_apply file
                     (conjectures, axiom_clauses, extra_clauses, helper_clauses,
-                     classrel_clauses, arity_clauses) =
+                     class_rel_clauses, arity_clauses) =
   let
     val axiom_lines = map (problem_line_for_axiom full_types) axiom_clauses
-    val classrel_lines = map problem_line_for_classrel classrel_clauses
-    val arity_lines = map problem_line_for_arity arity_clauses
+    val class_rel_lines =
+      map problem_line_for_class_rel_clause class_rel_clauses
+    val arity_lines = map problem_line_for_arity_clause arity_clauses
     val helper_lines = map (problem_line_for_axiom full_types) helper_clauses
     val conjecture_lines =
       map (problem_line_for_conjecture full_types) conjectures
     val tfree_lines = problem_lines_for_free_types conjectures
     val problem = [("Relevant facts", axiom_lines),
-                   ("Class relationships", classrel_lines),
+                   ("Class relationships", class_rel_lines),
                    ("Arity declarations", arity_lines),
                    ("Helper facts", helper_lines),
                    ("Conjectures", conjecture_lines),
@@ -321,9 +320,12 @@
                   |> repair_problem thy full_types explicit_apply
     val (problem, pool) = nice_problem problem (empty_name_pool readable_names)
     val conjecture_offset =
-      length axiom_lines + length classrel_lines + length arity_lines
+      length axiom_lines + length class_rel_lines + length arity_lines
       + length helper_lines
     val _ = File.write_list file (strings_for_problem problem)
-  in (pool, conjecture_offset) end
+  in
+    (case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
+     conjecture_offset)
+  end
 
 end;
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -584,8 +584,7 @@
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
 fun skolemize_prems_tac ctxt prems =
-    cut_facts_tac (skolemize_nnf_list ctxt prems) THEN'
-    REPEAT o (etac exE);
+  cut_facts_tac (skolemize_nnf_list ctxt prems) THEN' REPEAT o etac exE
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
   Function mkcl converts theorems to clauses.*)
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu Jul 22 16:53:00 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/Quickcheck_Examples.thy
-    ID:         $Id$
     Author:     Stefan Berghofer
     Copyright   2004 TU Muenchen
 *)
@@ -20,27 +19,27 @@
 subsection {* Lists *}
 
 theorem "map g (map f xs) = map (g o f) xs"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   oops
 
 theorem "map g (map f xs) = map (f o g) xs"
-  quickcheck
+  quickcheck[expect = counterexample]
   oops
 
 theorem "rev (xs @ ys) = rev ys @ rev xs"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   oops
 
 theorem "rev (xs @ ys) = rev xs @ rev ys"
-  quickcheck
+  quickcheck[expect = counterexample]
   oops
 
 theorem "rev (rev xs) = xs"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   oops
 
 theorem "rev xs = xs"
-  quickcheck
+  quickcheck[expect = counterexample]
   oops
 
 text {* An example involving functions inside other data structures *}
@@ -50,11 +49,11 @@
   | "app (f # fs) x = app fs (f x)"
 
 lemma "app (fs @ gs) x = app gs (app fs x)"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   by (induct fs arbitrary: x) simp_all
 
 lemma "app (fs @ gs) x = app fs (app gs x)"
-  quickcheck
+  quickcheck[expect = counterexample]
   oops
 
 primrec occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
@@ -68,16 +67,16 @@
 text {* A lemma, you'd think to be true from our experience with delAll *}
 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   -- {* Wrong. Precondition needed.*}
-  quickcheck
+  quickcheck[expect = counterexample]
   oops
 
 lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck
+  quickcheck[expect = counterexample]
     -- {* Also wrong.*}
   oops
 
 lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   by (induct xs) auto
 
 primrec replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -86,12 +85,12 @@
                             else (x#(replace a b xs)))"
 
 lemma "occurs a xs = occurs b (replace a b xs)"
-  quickcheck
+  quickcheck[expect = counterexample]
   -- {* Wrong. Precondition needed.*}
   oops
 
 lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
-  quickcheck
+  quickcheck[expect = no_counterexample]
   by (induct xs) simp_all
 
 
@@ -114,12 +113,12 @@
   | "mirror (Branch l r) = Branch (mirror r) (mirror l)"
 
 theorem "plant (rev (leaves xt)) = mirror xt"
-  quickcheck
+  quickcheck[expect = counterexample]
     --{* Wrong! *} 
   oops
 
 theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
-  quickcheck
+  quickcheck[expect = counterexample]
     --{* Wrong! *} 
   oops
 
@@ -134,7 +133,7 @@
   | "root (Node f x y) = f"
 
 theorem "hd (inOrder xt) = root xt"
-  quickcheck
+  quickcheck[expect = counterexample]
     --{* Wrong! *} 
   oops
 
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/ex/Quickcheck_Lattice_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Thu Jul 22 16:53:00 2010 +0200
@@ -0,0 +1,139 @@
+(*  Title:      HOL/ex/Quickcheck_Lattice_Examples.thy
+    Author:     Lukas Bulwahn
+    Copyright   2010 TU Muenchen
+*)
+
+theory Quickcheck_Lattice_Examples
+imports Quickcheck_Types
+begin
+
+text {* We show how other default types help to find counterexamples to propositions if
+  the standard default type @{typ int} is insufficient. *}
+
+notation
+  less_eq  (infix "\<sqsubseteq>" 50) and
+  less  (infix "\<sqsubset>" 50) and
+  top ("\<top>") and
+  bot ("\<bottom>") and
+  inf (infixl "\<sqinter>" 70) and
+  sup (infixl "\<squnion>" 65)
+
+subsection {* Distributive lattices *}
+
+lemma sup_inf_distrib2:
+ "((y :: 'a :: distrib_lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+  quickcheck[expect = no_counterexample]
+by(simp add: inf_sup_aci sup_inf_distrib1)
+
+lemma sup_inf_distrib2_1:
+ "((y :: 'a :: lattice) \<sqinter> z) \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma sup_inf_distrib2_2:
+ "((y :: 'a :: distrib_lattice) \<sqinter> z') \<squnion> x = (y \<squnion> x) \<sqinter> (z \<squnion> x)"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_sup_distrib1_1:
+ "(x :: 'a :: distrib_lattice) \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x' \<sqinter> z)"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_sup_distrib2_1:
+ "((y :: 'a :: distrib_lattice) \<squnion> z) \<sqinter> x = (y \<sqinter> x) \<squnion> (y \<sqinter> x)"
+  quickcheck[expect = counterexample]
+  oops
+
+subsection {* Bounded lattices *}
+
+lemma inf_bot_left [simp]:
+  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
+  quickcheck[expect = no_counterexample]
+  by (rule inf_absorb1) simp
+
+lemma inf_bot_left_1:
+  "\<bottom> \<sqinter> (x :: 'a :: bounded_lattice_bot) = x"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_bot_left_2:
+  "y \<sqinter> (x :: 'a :: bounded_lattice_bot) = \<bottom>"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_bot_left_3:
+  "x \<noteq> \<bottom> ==> y \<sqinter> (x :: 'a :: bounded_lattice_bot) \<noteq> \<bottom>"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_bot_right [simp]:
+  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = \<bottom>"
+  quickcheck[expect = no_counterexample]
+  by (rule inf_absorb2) simp
+
+lemma inf_bot_right_1:
+  "x \<noteq> \<bottom> ==> (x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> = y"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_bot_right_2:
+  "(x :: 'a :: bounded_lattice_bot) \<sqinter> \<bottom> ~= \<bottom>"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma inf_bot_right [simp]:
+  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = \<bottom>"
+  quickcheck[expect = counterexample]
+  oops
+
+lemma sup_bot_left [simp]:
+  "\<bottom> \<squnion> (x :: 'a :: bounded_lattice_bot) = x"
+  quickcheck[expect = no_counterexample]
+  by (rule sup_absorb2) simp
+
+lemma sup_bot_right [simp]:
+  "(x :: 'a :: bounded_lattice_bot) \<squnion> \<bottom> = x"
+  quickcheck[expect = no_counterexample]
+  by (rule sup_absorb1) simp
+
+lemma sup_eq_bot_iff [simp]:
+  "(x :: 'a :: bounded_lattice_bot) \<squnion> y = \<bottom> \<longleftrightarrow> x = \<bottom> \<and> y = \<bottom>"
+  quickcheck[expect = no_counterexample]
+  by (simp add: eq_iff)
+
+lemma sup_top_left [simp]:
+  "\<top> \<squnion> (x :: 'a :: bounded_lattice_top) = \<top>"
+  quickcheck[expect = no_counterexample]
+  by (rule sup_absorb1) simp
+
+lemma sup_top_right [simp]:
+  "(x :: 'a :: bounded_lattice_top) \<squnion> \<top> = \<top>"
+  quickcheck[expect = no_counterexample]
+  by (rule sup_absorb2) simp
+
+lemma inf_top_left [simp]:
+  "\<top> \<sqinter> x = (x :: 'a :: bounded_lattice_top)"
+  quickcheck[expect = no_counterexample]
+  by (rule inf_absorb2) simp
+
+lemma inf_top_right [simp]:
+  "x \<sqinter> \<top> = (x :: 'a :: bounded_lattice_top)"
+  quickcheck[expect = no_counterexample]
+  by (rule inf_absorb1) simp
+
+lemma inf_eq_top_iff [simp]:
+  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+  quickcheck[expect = no_counterexample]
+  by (simp add: eq_iff)
+
+
+no_notation
+  less_eq  (infix "\<sqsubseteq>" 50) and
+  less (infix "\<sqsubset>" 50) and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  top ("\<top>") and
+  bot ("\<bottom>")
+
+end
diff -r f18c4bc8b028 -r b8ca89c45086 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/HOL/ex/ROOT.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -59,6 +59,7 @@
   "HarmonicSeries",
   "Refute_Examples",
   "Quickcheck_Examples",
+  "Quickcheck_Lattice_Examples",
   "Landau",
   "Execute_Choice",
   "Summation",
diff -r f18c4bc8b028 -r b8ca89c45086 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/Tools/Code/code_scala.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -429,7 +429,8 @@
     (target, { serializer = isar_serializer, literals = literals,
       check = { env_var = "SCALA_HOME", make_destination = I,
         make_command = fn scala_home => fn p => fn _ =>
-          Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
+          "export JAVA_OPTS='-Xms128m -Xmx512m -Xss2m' && "
+            ^ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
   #> Code_Target.add_syntax_tyco target "fun"
      (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
         brackify_infix (1, R) fxy (
diff -r f18c4bc8b028 -r b8ca89c45086 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu Jul 22 16:43:21 2010 +0200
+++ b/src/Tools/quickcheck.ML	Thu Jul 22 16:53:00 2010 +0200
@@ -6,20 +6,27 @@
 
 signature QUICKCHECK =
 sig
+  val setup: theory -> theory
+  (* configuration *)
   val auto: bool Unsynchronized.ref
   val timing : bool Unsynchronized.ref
   datatype report = Report of
     { iterations : int, raised_match_errors : int,
       satisfied_assms : int list, positive_concl_tests : int }
+  datatype expectation = No_Expectation | No_Counterexample | Counterexample;
+  datatype test_params = Test_Params of
+  { size: int, iterations: int, default_type: typ list, no_assms: bool,
+    expect : expectation, report: bool, quiet : bool};
+  val test_params_of: theory -> test_params 
+  val add_generator:
+    string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
+      -> theory -> theory
+  (* testing terms and proof states *)
   val gen_test_term: Proof.context -> bool -> bool -> string option -> int -> int -> term ->
     (string * term) list option * ((string * int) list * ((int * report list) list) option)
   val test_term: Proof.context -> bool -> string option -> int -> int -> term ->
     (string * term) list option
-  val add_generator:
-    string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))
-      -> theory -> theory
-  val setup: theory -> theory
-  val quickcheck: (string * string) list -> int -> Proof.state -> (string * term) list option
+  val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
 end;
 
 structure Quickcheck : QUICKCHECK =
@@ -60,38 +67,49 @@
          (if null satisfied_assms then replicate (length assms) 0 else satisfied_assms),
       positive_concl_tests = if concl then positive_concl_tests + 1 else positive_concl_tests}
 
+(* expectation *)
+
+datatype expectation = No_Expectation | No_Counterexample | Counterexample; 
+
+fun merge_expectation (expect1, expect2) =
+  if expect1 = expect2 then expect1 else No_Expectation
+
 (* quickcheck configuration -- default parameters, test generators *)
 
 datatype test_params = Test_Params of
-  { size: int, iterations: int, default_type: typ option, no_assms: bool, report: bool, quiet : bool};
+  { size: int, iterations: int, default_type: typ list, no_assms: bool,
+  expect : expectation, report: bool, quiet : bool};
 
-fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
-  ((size, iterations), ((default_type, no_assms), (report, quiet)));
-fun make_test_params ((size, iterations), ((default_type, no_assms), (report, quiet))) =
+fun dest_test_params (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
+  ((size, iterations), ((default_type, no_assms), ((expect, report), quiet)));
+fun make_test_params ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))) =
   Test_Params { size = size, iterations = iterations, default_type = default_type,
-                no_assms = no_assms, report = report, quiet = quiet };
-fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, report, quiet }) =
-  make_test_params (f ((size, iterations), ((default_type, no_assms), (report, quiet))));
+                no_assms = no_assms, expect = expect, report = report, quiet = quiet };
+fun map_test_params f (Test_Params { size, iterations, default_type, no_assms, expect, report, quiet }) =
+  make_test_params (f ((size, iterations), ((default_type, no_assms), ((expect, report), quiet))));
 fun merge_test_params (Test_Params { size = size1, iterations = iterations1, default_type = default_type1,
-                                     no_assms = no_assms1, report = report1, quiet = quiet1 },
+                                     no_assms = no_assms1, expect = expect1, report = report1, quiet = quiet1 },
   Test_Params { size = size2, iterations = iterations2, default_type = default_type2,
-                no_assms = no_assms2, report = report2, quiet = quiet2 }) =
+                no_assms = no_assms2, expect = expect2, report = report2, quiet = quiet2 }) =
   make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
-    ((case default_type1 of NONE => default_type2 | _ => default_type1, no_assms1 orelse no_assms2),
-    (report1 orelse report2, quiet1 orelse quiet2)));
+    ((merge (op =) (default_type1, default_type2), no_assms1 orelse no_assms2),
+    ((merge_expectation (expect1, expect2), report1 orelse report2), quiet1 orelse quiet2)));
 
 structure Data = Theory_Data
 (
   type T = (string * (Proof.context -> bool -> term -> int -> term list option * (bool list * bool))) list
     * test_params;
   val empty = ([], Test_Params
-    { size = 10, iterations = 100, default_type = NONE, no_assms = false, report = false, quiet = false});
+    { size = 10, iterations = 100, default_type = [], no_assms = false,
+      expect = No_Expectation, report = false, quiet = false});
   val extend = I;
   fun merge ((generators1, params1), (generators2, params2)) : T =
     (AList.merge (op =) (K true) (generators1, generators2),
       merge_test_params (params1, params2));
 );
 
+val test_params_of = snd o Data.get;
+
 val add_generator = Data.map o apfst o AList.update (op =);
 
 (* generating tests *)
@@ -173,21 +191,26 @@
 fun test_term ctxt quiet generator_name size i t =
   fst (gen_test_term ctxt quiet false generator_name size i t)
 
+exception WELLSORTED of string
+
 fun monomorphic_term thy insts default_T = 
   let
     fun subst (T as TFree (v, S)) =
           let
             val T' = AList.lookup (op =) insts v
-              |> the_default (the_default T default_T)
-          in if Sign.of_sort thy (T, S) then T'
-            else error ("Type " ^ Syntax.string_of_typ_global thy T ^
+              |> the_default default_T
+          in if Sign.of_sort thy (T', S) then T'
+            else raise (WELLSORTED ("For instantiation with default_type " ^ Syntax.string_of_typ_global thy default_T ^
+              ":\n" ^ Syntax.string_of_typ_global thy T' ^
               " to be substituted for variable " ^
-              Syntax.string_of_typ_global thy T ^ "\ndoes not have sort " ^
-              Syntax.string_of_sort_global thy S)
+              Syntax.string_of_typ_global thy T ^ " does not have sort " ^
+              Syntax.string_of_sort_global thy S))
           end
       | subst T = T;
   in (map_types o map_atyps) subst end;
 
+datatype wellsorted_error = Wellsorted_Error of string | Term of term
+
 fun test_goal quiet report generator_name size iterations default_T no_assms insts i assms state =
   let
     val ctxt = Proof.context_of state;
@@ -198,9 +221,23 @@
     val (gi, frees) = Logic.goal_params (prop_of st) i;
     val gi' = Logic.list_implies (if no_assms then [] else assms,
                                   subst_bounds (frees, strip gi))
-      |> monomorphic_term thy insts default_T
-      |> Object_Logic.atomize_term thy;
-  in gen_test_term ctxt quiet report generator_name size iterations gi' end;
+    val inst_goals = map (fn T =>
+      Term (monomorphic_term thy insts T gi |> Object_Logic.atomize_term thy)
+        handle WELLSORTED s => Wellsorted_Error s) default_T
+    val error_msg = cat_lines (map_filter (fn Term t => NONE | Wellsorted_Error s => SOME s) inst_goals)
+    val correct_inst_goals =
+      case map_filter (fn Term t => SOME t | Wellsorted_Error s => NONE) inst_goals of
+        [] => error error_msg
+      | xs => xs
+    val _ = if quiet then () else warning error_msg
+    fun collect_results f reports [] = (NONE, rev reports)
+      | collect_results f reports (t :: ts) =
+        case f t of
+          (SOME res, report) => (SOME res, rev (report :: reports))
+        | (NONE, report) => collect_results f (report :: reports) ts
+  in collect_results (gen_test_term ctxt quiet report generator_name size iterations) [] correct_inst_goals end;
+
+(* pretty printing *)
 
 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."
   | pretty_counterex ctxt (SOME cex) =
@@ -233,8 +270,8 @@
       (rev reports))
   | pretty_reports ctxt NONE = Pretty.str ""
 
-fun pretty_counterex_and_reports ctxt (cex, (timing, reports)) =
-  Pretty.chunks [pretty_counterex ctxt cex, pretty_reports ctxt reports]
+fun pretty_counterex_and_reports ctxt (cex, timing_and_reports) =
+  Pretty.chunks (pretty_counterex ctxt cex :: map (pretty_reports ctxt) (map snd timing_and_reports))
 
 (* automatic testing *)
 
@@ -245,7 +282,7 @@
     let
       val ctxt = Proof.context_of state;
       val assms = map term_of (Assumption.all_assms_of ctxt);
-      val Test_Params { size, iterations, default_type, no_assms, report, quiet } =
+      val Test_Params {size, iterations, default_type, no_assms, ...} =
         (snd o Data.get o Proof.theory_of) state;
       val res =
         try (test_goal true false NONE size iterations default_type no_assms [] 1 assms) state;
@@ -266,31 +303,39 @@
  of (k, []) => if k >= 0 then k
       else error ("Not a natural number: " ^ s)
   | (_, _ :: _) => error ("Not a natural number: " ^ s);
+
 fun read_bool "false" = false
   | read_bool "true" = true
   | read_bool s = error ("Not a Boolean value: " ^ s)
 
-fun parse_test_param ctxt ("size", arg) =
+fun read_expectation "no_expectation" = No_Expectation
+  | read_expectation "no_counterexample" = No_Counterexample 
+  | read_expectation "counterexample" = Counterexample
+  | read_expectation s = error ("Not an expectation value: " ^ s)  
+
+fun parse_test_param ctxt ("size", [arg]) =
       (apfst o apfst o K) (read_nat arg)
-  | parse_test_param ctxt ("iterations", arg) =
+  | parse_test_param ctxt ("iterations", [arg]) =
       (apfst o apsnd o K) (read_nat arg)
   | parse_test_param ctxt ("default_type", arg) =
-      (apsnd o apfst o apfst o K o SOME) (ProofContext.read_typ ctxt arg)
-  | parse_test_param ctxt ("no_assms", arg) =
+      (apsnd o apfst o apfst o K) (map (ProofContext.read_typ ctxt) arg)
+  | parse_test_param ctxt ("no_assms", [arg]) =
       (apsnd o apfst o apsnd o K) (read_bool arg)
-  | parse_test_param ctxt ("report", arg) =
-      (apsnd o apsnd o apfst o K) (read_bool arg)
-  | parse_test_param ctxt ("quiet", arg) =
-      (apsnd o apsnd o apsnd o K) (read_bool arg)
+  | parse_test_param ctxt ("expect", [arg]) =
+      (apsnd o apsnd o apfst o apfst o K) (read_expectation arg)
+  | parse_test_param ctxt ("report", [arg]) =
+      (apsnd o apsnd o apfst o apsnd o K) (read_bool arg)
+  | parse_test_param ctxt ("quiet", [arg]) =
+      (apsnd o apsnd o apsnd o K) (read_bool arg)       
   | parse_test_param ctxt (name, _) =
       error ("Unknown test parameter: " ^ name);
 
-fun parse_test_param_inst ctxt ("generator", arg) =
+fun parse_test_param_inst ctxt ("generator", [arg]) =
       (apsnd o apfst o K o SOME) arg
   | parse_test_param_inst ctxt (name, arg) =
       case try (ProofContext.read_typ ctxt) name
        of SOME (TFree (v, _)) => (apsnd o apsnd o AList.update (op =))
-              (v, ProofContext.read_typ ctxt arg)
+              (v, ProofContext.read_typ ctxt (the_single arg))
         | _ => (apfst o parse_test_param ctxt) (name, arg);
 
 fun quickcheck_params_cmd args thy =
@@ -309,10 +354,14 @@
     val assms = map term_of (Assumption.all_assms_of ctxt);
     val default_params = (dest_test_params o snd o Data.get) thy;
     val f = fold (parse_test_param_inst ctxt) args;
-    val (((size, iterations), ((default_type, no_assms), (report, quiet))), (generator_name, insts)) =
+    val (((size, iterations), ((default_type, no_assms), ((expect, report), quiet))), (generator_name, insts)) =
       f (default_params, (NONE, []));
   in
     test_goal quiet report generator_name size iterations default_type no_assms insts i assms state
+    |> tap (fn (SOME x, _) => if expect = No_Counterexample then
+                 error ("quickcheck expect to find no counterexample but found one") else ()
+             | (NONE, _) => if expect = Counterexample then
+                 error ("quickcheck expected to find a counterexample but did not find one") else ())
   end;
 
 fun quickcheck args i state = fst (gen_quickcheck args i state);
@@ -321,7 +370,8 @@
   gen_quickcheck args i (Toplevel.proof_of state)
   |> Pretty.writeln o pretty_counterex_and_reports (Toplevel.context_of state);
 
-val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- Parse.name) "true");
+val parse_arg = Parse.name -- (Scan.optional (Parse.$$$ "=" |-- 
+  ((Parse.name >> single) || (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"))) ["true"]);
 
 val parse_args = Parse.$$$ "[" |-- Parse.list1 parse_arg --| Parse.$$$ "]"
   || Scan.succeed [];