# HG changeset patch
# User paulson
# Date 1258112045 0
# Node ID c6dde2106128d4022fe03a442efc1165910eb74e
# Parent  feaf3627a844096d59508fbf71cbe009e5a15fa3# Parent  abf780db30eadfb1c50a8e346d2cd347e13f458d
merged

diff -r abf780db30ea -r c6dde2106128 CONTRIBUTORS
--- a/CONTRIBUTORS	Fri Nov 13 11:33:33 2009 +0000
+++ b/CONTRIBUTORS	Fri Nov 13 11:34:05 2009 +0000
@@ -6,6 +6,10 @@
 
 Contributions to this Isabelle version
 --------------------------------------
+
+* November 2009: Stefan Berghofer, Lukas Bulwahn, TUM
+  A tabled implementation of the reflexive transitive closure
+
 * November 2009: Lukas Bulwahn, TUM
   Predicate Compiler: a compiler for inductive predicates to equational specfications
  
diff -r abf780db30ea -r c6dde2106128 NEWS
--- a/NEWS	Fri Nov 13 11:33:33 2009 +0000
+++ b/NEWS	Fri Nov 13 11:34:05 2009 +0000
@@ -37,6 +37,8 @@
 
 *** HOL ***
 
+* A tabled implementation of the reflexive transitive closure
+
 * New commands "code_pred" and "values" to invoke the predicate compiler
 and to enumerate values of inductive predicates.
 
diff -r abf780db30ea -r c6dde2106128 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/IsaMakefile	Fri Nov 13 11:34:05 2009 +0000
@@ -382,8 +382,9 @@
   Library/Order_Relation.thy Library/Nested_Environment.thy		\
   Library/Ramsey.thy Library/Zorn.thy Library/Library/ROOT.ML		\
   Library/Library/document/root.tex Library/Library/document/root.bib	\
-  Library/While_Combinator.thy Library/Product_ord.thy			\
-  Library/Char_nat.thy Library/Char_ord.thy Library/Option_ord.thy	\
+  Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
+  Library/Product_ord.thy	Library/Char_nat.thy \
+  Library/Char_ord.thy Library/Option_ord.thy	\
   Library/Sublist_Order.thy Library/List_lexord.thy			\
   Library/Coinductive_List.thy Library/AssocList.thy			\
   Library/Formal_Power_Series.thy Library/Binomial.thy			\
diff -r abf780db30ea -r c6dde2106128 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Library/Library.thy	Fri Nov 13 11:34:05 2009 +0000
@@ -51,6 +51,7 @@
   SML_Quickcheck
   State_Monad
   Sum_Of_Squares
+  Transitive_Closure_Table
   Univ_Poly
   While_Combinator
   Word
diff -r abf780db30ea -r c6dde2106128 src/HOL/Library/Transitive_Closure_Table.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Transitive_Closure_Table.thy	Fri Nov 13 11:34:05 2009 +0000
@@ -0,0 +1,230 @@
+(* Author: Stefan Berghofer, Lukas Bulwahn, TU Muenchen *)
+
+header {* A tabled implementation of the reflexive transitive closure *}
+
+theory Transitive_Closure_Table
+imports Main
+begin
+
+inductive rtrancl_path :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "rtrancl_path r x [] x"
+| step: "r x y \<Longrightarrow> rtrancl_path r y ys z \<Longrightarrow> rtrancl_path r x (y # ys) z"
+
+lemma rtranclp_eq_rtrancl_path: "r\<^sup>*\<^sup>* x y = (\<exists>xs. rtrancl_path r x xs y)"
+proof
+  assume "r\<^sup>*\<^sup>* x y"
+  then show "\<exists>xs. rtrancl_path r x xs y"
+  proof (induct rule: converse_rtranclp_induct)
+    case 1
+    have "rtrancl_path r y [] y" by (rule rtrancl_path.base)
+    then show ?case ..
+  next
+    case (2 x z)
+    from `\<exists>xs. rtrancl_path r z xs y`
+    obtain xs where "rtrancl_path r z xs y" ..
+    with `r x z` have "rtrancl_path r x (z # xs) y"
+      by (rule rtrancl_path.step)
+    then show ?case ..
+  qed
+next
+  assume "\<exists>xs. rtrancl_path r x xs y"
+  then obtain xs where "rtrancl_path r x xs y" ..
+  then show "r\<^sup>*\<^sup>* x y"
+  proof induct
+    case (base x)
+    show ?case by (rule rtranclp.rtrancl_refl)
+  next
+    case (step x y ys z)
+    from `r x y` `r\<^sup>*\<^sup>* y z` show ?case
+      by (rule converse_rtranclp_into_rtranclp)
+  qed
+qed
+
+lemma rtrancl_path_trans:
+  assumes xy: "rtrancl_path r x xs y"
+  and yz: "rtrancl_path r y ys z"
+  shows "rtrancl_path r x (xs @ ys) z" using xy yz
+proof (induct arbitrary: z)
+  case (base x)
+  then show ?case by simp
+next
+  case (step x y xs)
+  then have "rtrancl_path r y (xs @ ys) z"
+    by simp
+  with `r x y` have "rtrancl_path r x (y # (xs @ ys)) z"
+    by (rule rtrancl_path.step)
+  then show ?case by simp
+qed
+
+lemma rtrancl_path_appendE:
+  assumes xz: "rtrancl_path r x (xs @ y # ys) z"
+  obtains "rtrancl_path r x (xs @ [y]) y" and "rtrancl_path r y ys z" using xz
+proof (induct xs arbitrary: x)
+  case Nil
+  then have "rtrancl_path r x (y # ys) z" by simp
+  then obtain xy: "r x y" and yz: "rtrancl_path r y ys z"
+    by cases auto
+  from xy have "rtrancl_path r x [y] y"
+    by (rule rtrancl_path.step [OF _ rtrancl_path.base])
+  then have "rtrancl_path r x ([] @ [y]) y" by simp
+  then show ?thesis using yz by (rule Nil)
+next
+  case (Cons a as)
+  then have "rtrancl_path r x (a # (as @ y # ys)) z" by simp
+  then obtain xa: "r x a" and az: "rtrancl_path r a (as @ y # ys) z"
+    by cases auto
+  show ?thesis
+  proof (rule Cons(1) [OF _ az])
+    assume "rtrancl_path r y ys z"
+    assume "rtrancl_path r a (as @ [y]) y"
+    with xa have "rtrancl_path r x (a # (as @ [y])) y"
+      by (rule rtrancl_path.step)
+    then have "rtrancl_path r x ((a # as) @ [y]) y"
+      by simp
+    then show ?thesis using `rtrancl_path r y ys z`
+      by (rule Cons(2))
+  qed
+qed
+
+lemma rtrancl_path_distinct:
+  assumes xy: "rtrancl_path r x xs y"
+  obtains xs' where "rtrancl_path r x xs' y" and "distinct (x # xs')" using xy
+proof (induct xs rule: measure_induct_rule [of length])
+  case (less xs)
+  show ?case
+  proof (cases "distinct (x # xs)")
+    case True
+    with `rtrancl_path r x xs y` show ?thesis by (rule less)
+  next
+    case False
+    then have "\<exists>as bs cs a. x # xs = as @ [a] @ bs @ [a] @ cs"
+      by (rule not_distinct_decomp)
+    then obtain as bs cs a where xxs: "x # xs = as @ [a] @ bs @ [a] @ cs"
+      by iprover
+    show ?thesis
+    proof (cases as)
+      case Nil
+      with xxs have x: "x = a" and xs: "xs = bs @ a # cs"
+	by auto
+      from x xs `rtrancl_path r x xs y` have cs: "rtrancl_path r x cs y"
+	by (auto elim: rtrancl_path_appendE)
+      from xs have "length cs < length xs" by simp
+      then show ?thesis
+	by (rule less(1)) (iprover intro: cs less(2))+
+    next
+      case (Cons d ds)
+      with xxs have xs: "xs = ds @ a # (bs @ [a] @ cs)"
+	by auto
+      with `rtrancl_path r x xs y` obtain xa: "rtrancl_path r x (ds @ [a]) a"
+        and ay: "rtrancl_path r a (bs @ a # cs) y"
+	by (auto elim: rtrancl_path_appendE)
+      from ay have "rtrancl_path r a cs y" by (auto elim: rtrancl_path_appendE)
+      with xa have xy: "rtrancl_path r x ((ds @ [a]) @ cs) y"
+	by (rule rtrancl_path_trans)
+      from xs have "length ((ds @ [a]) @ cs) < length xs" by simp
+      then show ?thesis
+	by (rule less(1)) (iprover intro: xy less(2))+
+    qed
+  qed
+qed
+
+inductive rtrancl_tab :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
+  for r :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+where
+  base: "rtrancl_tab r xs x x"
+| step: "x \<notin> set xs \<Longrightarrow> r x y \<Longrightarrow> rtrancl_tab r (x # xs) y z \<Longrightarrow> rtrancl_tab r xs x z"
+
+lemma rtrancl_path_imp_rtrancl_tab:
+  assumes path: "rtrancl_path r x xs y"
+  and x: "distinct (x # xs)"
+  and ys: "({x} \<union> set xs) \<inter> set ys = {}"
+  shows "rtrancl_tab r ys x y" using path x ys
+proof (induct arbitrary: ys)
+  case base
+  show ?case by (rule rtrancl_tab.base)
+next
+  case (step x y zs z)
+  then have "x \<notin> set ys" by auto
+  from step have "distinct (y # zs)" by simp
+  moreover from step have "({y} \<union> set zs) \<inter> set (x # ys) = {}"
+    by auto
+  ultimately have "rtrancl_tab r (x # ys) y z"
+    by (rule step)
+  with `x \<notin> set ys` `r x y`
+  show ?case by (rule rtrancl_tab.step)
+qed
+
+lemma rtrancl_tab_imp_rtrancl_path:
+  assumes tab: "rtrancl_tab r ys x y"
+  obtains xs where "rtrancl_path r x xs y" using tab
+proof induct
+  case base
+  from rtrancl_path.base show ?case by (rule base)
+next
+  case step show ?case by (iprover intro: step rtrancl_path.step)
+qed
+
+lemma rtranclp_eq_rtrancl_tab_nil: "r\<^sup>*\<^sup>* x y = rtrancl_tab r [] x y"
+proof
+  assume "r\<^sup>*\<^sup>* x y"
+  then obtain xs where "rtrancl_path r x xs y"
+    by (auto simp add: rtranclp_eq_rtrancl_path)
+  then obtain xs' where xs': "rtrancl_path r x xs' y"
+    and distinct: "distinct (x # xs')"
+    by (rule rtrancl_path_distinct)
+  have "({x} \<union> set xs') \<inter> set [] = {}" by simp
+  with xs' distinct show "rtrancl_tab r [] x y"
+    by (rule rtrancl_path_imp_rtrancl_tab)
+next
+  assume "rtrancl_tab r [] x y"
+  then obtain xs where "rtrancl_path r x xs y"
+    by (rule rtrancl_tab_imp_rtrancl_path)
+  then show "r\<^sup>*\<^sup>* x y"
+    by (auto simp add: rtranclp_eq_rtrancl_path)
+qed
+
+declare rtranclp_eq_rtrancl_tab_nil [code_unfold]
+
+declare rtranclp_eq_rtrancl_tab_nil[THEN iffD2, code_pred_intro]
+
+code_pred rtranclp using rtranclp_eq_rtrancl_tab_nil[THEN iffD1] by fastsimp
+
+subsection {* A simple example *}
+
+datatype ty = A | B | C
+
+inductive test :: "ty \<Rightarrow> ty \<Rightarrow> bool"
+where
+  "test A B"
+| "test B A"
+| "test B C"
+
+subsubsection {* Invoking with the SML code generator *}
+
+code_module Test
+contains
+test1 = "test\<^sup>*\<^sup>* A C"
+test2 = "test\<^sup>*\<^sup>* C A"
+test3 = "test\<^sup>*\<^sup>* A _"
+test4 = "test\<^sup>*\<^sup>* _ C"
+
+ML "Test.test1"
+ML "Test.test2"
+ML "DSeq.list_of Test.test3"
+ML "DSeq.list_of Test.test4"
+
+subsubsection {* Invoking with the predicate compiler and the generic code generator *}
+
+code_pred test .
+
+values "{x. test\<^sup>*\<^sup>* A C}"
+values "{x. test\<^sup>*\<^sup>* C A}"
+values "{x. test\<^sup>*\<^sup>* A x}"
+values "{x. test\<^sup>*\<^sup>* x C}"
+
+hide const test
+
+end
+
diff -r abf780db30ea -r c6dde2106128 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -569,7 +569,7 @@
       thy3
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = false, verbose = false, kind = Thm.internalK,
+          {quiet_mode = false, verbose = false, kind = "",
            alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
@@ -1513,7 +1513,7 @@
       thy10
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = "",
            alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -156,7 +156,7 @@
       thy0
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = "",
             alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
             skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -175,7 +175,7 @@
       thy1
       |> Sign.map_naming Name_Space.conceal
       |> Inductive.add_inductive_global (serial ())
-          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+          {quiet_mode = #quiet config, verbose = false, kind = "",
            alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
            skip_mono = true, fork_mono = false}
           (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Function/function_core.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -460,7 +460,7 @@
       |> Inductive.add_inductive_i
           {quiet_mode = true,
             verbose = ! trace,
-            kind = Thm.internalK,
+            kind = "",
             alt_name = Binding.empty,
             coind = false,
             no_elim = false,
@@ -519,7 +519,7 @@
         $ (default $ Bound 0) $ Abs ("y", ranT, G $ Bound 1 $ Bound 0))
       |> Syntax.check_term lthy
   in
-    LocalTheory.define Thm.internalK
+    LocalTheory.define ""
       ((Binding.name (function_name fname), mixfix),
         ((Binding.conceal (Binding.name fdefname), []), f_def)) lthy
   end
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -146,7 +146,7 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.define Thm.internalK
+              LocalTheory.define ""
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -1047,7 +1047,6 @@
     let
       val _ = tracing ("Clause " ^ string_of_int (i + 1) ^ " of " ^
       p ^ " violates mode " ^ string_of_mode thy p m)
-      val _ = tracing (string_of_clause thy p (nth rs i))
     in () end
   else ()
 
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -355,7 +355,7 @@
               thy
               |> Sign.map_naming Name_Space.conceal
               |> Inductive.add_inductive_global (serial ())
-                {quiet_mode = false, verbose = false, kind = Thm.internalK,
+                {quiet_mode = false, verbose = false, kind = "",
                   alt_name = Binding.empty, coind = false, no_elim = false,
                   no_ind = false, skip_mono = false, fork_mono = false}
                 (map (fn (s, T) =>
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -23,6 +23,8 @@
 
 val options = Options {
   expected_modes = NONE,
+  proposed_modes = [],
+  proposed_names = [],
   show_steps = true,
   show_intermediate_results = true,
   show_proof_trace = false,
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/inductive.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -663,7 +663,7 @@
 
     val ((rec_const, (_, fp_def)), lthy') = lthy
       |> LocalTheory.conceal
-      |> LocalTheory.define Thm.internalK
+      |> LocalTheory.define ""
         ((rec_name, case cnames_syn of [(_, syn)] => syn | _ => NoSyn),
          ((Binding.empty, [Attrib.internal (K Nitpick_Defs.add)]),
          fold_rev lambda params
@@ -686,13 +686,13 @@
           end) (cnames_syn ~~ cs);
     val (consts_defs, lthy'') = lthy'
       |> LocalTheory.conceal
-      |> fold_map (LocalTheory.define Thm.internalK) specs
+      |> fold_map (LocalTheory.define "") specs
       ||> LocalTheory.restore_naming lthy';
     val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
 
     val mono = prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos lthy'';
     val ((_, [mono']), lthy''') =
-      LocalTheory.note Thm.internalK (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
+      LocalTheory.note "" (apfst Binding.conceal Attrib.empty_binding, [mono]) lthy'';
 
   in (lthy''', rec_name, mono', fp_def', map (#2 o #2) consts_defs,
     list_comb (rec_const, params), preds, argTs, bs, xs)
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -485,7 +485,7 @@
     (* define inductive sets using previously defined predicates *)
     val (defs, lthy2) = lthy1
       |> LocalTheory.conceal  (* FIXME ?? *)
-      |> fold_map (LocalTheory.define Thm.internalK)
+      |> fold_map (LocalTheory.define "")
         (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
            fold_rev lambda params (HOLogic.Collect_const U $
              HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/recdef.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -263,7 +263,7 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    Specification.theorem Thm.internalK NONE (K I)
+    Specification.theorem "" NONE (K I)
       (Binding.conceal (Binding.name bname), atts) []
       (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
diff -r abf780db30ea -r c6dde2106128 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/Tools/res_atp.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -352,20 +352,32 @@
       filter (not o known) c_clauses
   end;
 
-fun valid_facts facts =
-  Facts.fold_static (fn (name, ths) =>
-    if Facts.is_concealed facts name orelse
-      (run_blacklist_filter andalso is_package_def name) then I
-    else
-      let val xname = Facts.extern facts name in
-        if Name_Space.is_hidden xname then I
-        else cons (xname, filter_out Res_Axioms.bad_for_atp ths)
-      end) facts [];
-
 fun all_valid_thms ctxt =
   let
     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
     val local_facts = ProofContext.facts_of ctxt;
+    val full_space =
+      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
+
+    fun valid_facts facts =
+      (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
+        let
+          fun check_thms a =
+            (case try (ProofContext.get_thms ctxt) a of
+              NONE => false
+            | SOME ths1 => Thm.eq_thms (ths0, ths1));
+
+          val name1 = Facts.extern facts name;
+          val name2 = Name_Space.extern full_space name;
+          val ths = filter_out Res_Axioms.bad_for_atp ths0;
+        in
+          if Facts.is_concealed facts name orelse null ths orelse
+            run_blacklist_filter andalso is_package_def name then I
+          else
+            (case find_first check_thms [name1, name2, name] of
+              NONE => I
+            | SOME a => cons (a, ths))
+        end);
   in valid_facts global_facts @ valid_facts local_facts end;
 
 fun multi_name a th (n, pairs) =
diff -r abf780db30ea -r c6dde2106128 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOL/ex/ROOT.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -13,7 +13,8 @@
   "Codegenerator_Pretty_Test",
   "NormalForm",
   "Predicate_Compile",
-  "Predicate_Compile_ex"
+  "Predicate_Compile_ex",
+  "Predicate_Compile_Quickcheck"
 ];
 
 use_thys [
diff -r abf780db30ea -r c6dde2106128 src/HOLCF/Tools/pcpodef.ML
--- a/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/HOLCF/Tools/pcpodef.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -7,14 +7,31 @@
 
 signature PCPODEF =
 sig
+  type cpo_info =
+    { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+      lub: thm, thelub: thm, compact: thm }
+  type pcpo_info =
+    { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+      Rep_defined: thm, Abs_defined: thm }
+
+  val add_podef: bool -> binding option -> binding * string list * mixfix ->
+    term -> (binding * binding) option -> tactic -> theory ->
+    (Typedef.info * thm) * theory
+  val add_cpodef: bool -> binding option -> binding * string list * mixfix ->
+    term -> (binding * binding) option -> tactic * tactic -> theory ->
+    (Typedef.info * cpo_info) * theory
+  val add_pcpodef: bool -> binding option -> binding * string list * mixfix ->
+    term -> (binding * binding) option -> tactic * tactic -> theory ->
+    (Typedef.info * cpo_info * pcpo_info) * theory
+
+  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
+    * (binding * binding) option -> theory -> Proof.state
+  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
+    * (binding * binding) option -> theory -> Proof.state
   val pcpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
     * (binding * binding) option -> theory -> Proof.state
   val pcpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
     * (binding * binding) option -> theory -> Proof.state
-  val cpodef_proof: (bool * binding) * (binding * string list * mixfix) * term
-    * (binding * binding) option -> theory -> Proof.state
-  val cpodef_proof_cmd: (bool * binding) * (binding * string list * mixfix) * string
-    * (binding * binding) option -> theory -> Proof.state
 end;
 
 structure Pcpodef :> PCPODEF =
@@ -22,22 +39,124 @@
 
 (** type definitions **)
 
-(* prepare_cpodef *)
+type cpo_info =
+  { below_def: thm, adm: thm, cont_Rep: thm, cont_Abs: thm,
+    lub: thm, thelub: thm, compact: thm }
 
-fun declare_type_name a = Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+type pcpo_info =
+  { Rep_strict: thm, Abs_strict: thm, Rep_strict_iff: thm, Abs_strict_iff: thm,
+    Rep_defined: thm, Abs_defined: thm }
+
+(* building terms *)
 
 fun adm_const T = Const (@{const_name adm}, (T --> HOLogic.boolT) --> HOLogic.boolT);
 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T, P);
 
-fun prepare_pcpodef prep_term pcpo def name (t, vs, mx) raw_set opt_morphs thy =
+fun below_const T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
+
+(* manipulating theorems *)
+
+fun fold_adm_mem thm NONE = thm
+  | fold_adm_mem thm (SOME set_def) =
+    let val rule = @{lemma "A == B ==> adm (%x. x : B) ==> adm (%x. x : A)" by simp}
+    in rule OF [set_def, thm] end;
+
+fun fold_UU_mem thm NONE = thm
+  | fold_UU_mem thm (SOME set_def) =
+    let val rule = @{lemma "A == B ==> UU : B ==> UU : A" by simp}
+    in rule OF [set_def, thm] end;
+
+(* proving class instances *)
+
+fun prove_cpo
+      (name: binding)
+      (newT: typ)
+      (Rep_name: binding, Abs_name: binding)
+      (type_definition: thm)  (* type_definition Rep Abs A *)
+      (set_def: thm option)   (* A == set *)
+      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
+      (admissible: thm)       (* adm (%x. x : set) *)
+      (thy: theory)
+    =
+  let
+    val admissible' = fold_adm_mem admissible set_def;
+    val cpo_thms = map (Thm.transfer thy) [type_definition, below_def, admissible'];
+    val (full_tname, Ts) = dest_Type newT;
+    val lhs_sorts = map (snd o dest_TFree) Ts;
+    val thy2 =
+      thy
+      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
+          (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
+    val cpo_thms' = map (Thm.transfer thy2) cpo_thms;
+    fun make thm = Drule.standard (thm OF cpo_thms');
+    val ([adm, cont_Rep, cont_Abs, lub, thelub, compact], thy3) =
+      thy2
+      |> Sign.add_path (Binding.name_of name)
+      |> PureThy.add_thms
+        ([((Binding.prefix_name "adm_" name, admissible'), []),
+          ((Binding.prefix_name "cont_" Rep_name, make @{thm typedef_cont_Rep}), []),
+          ((Binding.prefix_name "cont_" Abs_name, make @{thm typedef_cont_Abs}), []),
+          ((Binding.prefix_name "lub_" name, make @{thm typedef_lub}), []),
+          ((Binding.prefix_name "thelub_" name, make @{thm typedef_thelub}), []),
+          ((Binding.prefix_name "compact_" name, make @{thm typedef_compact}), [])])
+      ||> Sign.parent_path;
+    val cpo_info : cpo_info =
+      { below_def = below_def, adm = admissible', cont_Rep = cont_Rep,
+        cont_Abs = cont_Abs, lub = lub, thelub = thelub, compact = compact };
+  in
+    (cpo_info, thy3)
+  end;
+
+fun prove_pcpo
+      (name: binding)
+      (newT: typ)
+      (Rep_name: binding, Abs_name: binding)
+      (type_definition: thm)  (* type_definition Rep Abs A *)
+      (set_def: thm option)   (* A == set *)
+      (below_def: thm)        (* op << == %x y. Rep x << Rep y *)
+      (UU_mem: thm)           (* UU : set *)
+      (thy: theory)
+    =
+  let
+    val UU_mem' = fold_UU_mem UU_mem set_def;
+    val pcpo_thms = map (Thm.transfer thy) [type_definition, below_def, UU_mem'];
+    val (full_tname, Ts) = dest_Type newT;
+    val lhs_sorts = map (snd o dest_TFree) Ts;
+    val thy2 = thy
+      |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
+        (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
+    val pcpo_thms' = map (Thm.transfer thy2) pcpo_thms;
+    fun make thm = Drule.standard (thm OF pcpo_thms');
+    val ([Rep_strict, Abs_strict, Rep_strict_iff, Abs_strict_iff,
+          Rep_defined, Abs_defined], thy3) =
+      thy2
+      |> Sign.add_path (Binding.name_of name)
+      |> PureThy.add_thms
+        ([((Binding.suffix_name "_strict" Rep_name, make @{thm typedef_Rep_strict}), []),
+          ((Binding.suffix_name "_strict" Abs_name, make @{thm typedef_Abs_strict}), []),
+          ((Binding.suffix_name "_strict_iff" Rep_name, make @{thm typedef_Rep_strict_iff}), []),
+          ((Binding.suffix_name "_strict_iff" Abs_name, make @{thm typedef_Abs_strict_iff}), []),
+          ((Binding.suffix_name "_defined" Rep_name, make @{thm typedef_Rep_defined}), []),
+          ((Binding.suffix_name "_defined" Abs_name, make @{thm typedef_Abs_defined}), [])])
+      ||> Sign.parent_path;
+    val pcpo_info =
+      { Rep_strict = Rep_strict, Abs_strict = Abs_strict,
+        Rep_strict_iff = Rep_strict_iff, Abs_strict_iff = Abs_strict_iff,
+        Rep_defined = Rep_defined, Abs_defined = Abs_defined };
+  in
+    (pcpo_info, thy3)
+  end;
+
+(* prepare_cpodef *)
+
+fun declare_type_name a =
+  Variable.declare_constraints (Logic.mk_type (TFree (a, dummyS)));
+
+fun prepare prep_term _ name (t, vs, mx) raw_set opt_morphs thy =
   let
     val _ = Theory.requires thy "Pcpodef" "pcpodefs";
     val ctxt = ProofContext.init thy;
 
-    val full = Sign.full_name thy;
-    val full_name = full name;
-    val bname = Binding.name_of name;
-
     (*rhs*)
     val set = prep_term (ctxt |> fold declare_type_name vs) raw_set;
     val setT = Term.fastype_of set;
@@ -45,129 +164,171 @@
     val oldT = HOLogic.dest_setT setT handle TYPE _ =>
       error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
 
-    (*goal*)
-    val goal_UU_mem = HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+    (*lhs*)
+    val defS = Sign.defaultS thy;
+    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
+    val lhs_sorts = map snd lhs_tfrees;
+    val tname = Binding.map_name (Syntax.type_name mx) t;
+    val full_tname = Sign.full_name thy tname;
+    val newT = Type (full_tname, map TFree lhs_tfrees);
+
+    val morphs = opt_morphs
+      |> the_default (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name);
+  in
+    (newT, oldT, set, morphs, lhs_sorts)
+  end
+
+fun add_podef def opt_name typ set opt_morphs tac thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val ((full_tname, info as {type_definition, set_def, Rep_name, ...}), thy2) = thy
+      |> Typedef.add_typedef def opt_name typ set opt_morphs tac;
+    val oldT = #rep_type info;
+    val newT = #abs_type info;
+    val lhs_tfrees = map dest_TFree (snd (dest_Type newT));
+
+    val RepC = Const (Rep_name, newT --> oldT);
+    val below_def = Logic.mk_equals (below_const newT,
+      Abs ("x", newT, Abs ("y", newT, below_const oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
+    val lthy3 = thy2
+      |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
+    val below_def' = Syntax.check_term lthy3 below_def;
+    val ((_, (_, below_definition')), lthy4) = lthy3
+      |> Specification.definition (NONE,
+          ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
+    val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
+    val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
+    val thy5 = lthy4
+      |> Class.prove_instantiation_instance
+          (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
+      |> LocalTheory.exit_global;
+  in ((info, below_definition), thy5) end;
+
+fun prepare_cpodef
+      (prep_term: Proof.context -> 'a -> term)
+      (def: bool)
+      (name: binding)
+      (typ: binding * string list * mixfix)
+      (raw_set: 'a)
+      (opt_morphs: (binding * binding) option)
+      (thy: theory)
+    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info) * theory) =
+  let
+    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
+      prepare prep_term def name typ raw_set opt_morphs thy;
+
     val goal_nonempty =
       HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
     val goal_admissible =
       HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
 
-    (*lhs*)
-    val defS = Sign.defaultS thy;
-    val lhs_tfrees = map (fn v => (v, the_default defS (AList.lookup (op =) rhs_tfrees v))) vs;
-    val lhs_sorts = map snd lhs_tfrees;
-
-    val tname = Binding.map_name (Syntax.type_name mx) t;
-    val full_tname = full tname;
-    val newT = Type (full_tname, map TFree lhs_tfrees);
-
-    val (Rep_name, Abs_name) =
-      (case opt_morphs of
-        NONE => (Binding.prefix_name "Rep_" name, Binding.prefix_name "Abs_" name)
-      | SOME morphs => morphs);
-    val RepC = Const (full Rep_name, newT --> oldT);
-    fun belowC T = Const (@{const_name below}, T --> T --> HOLogic.boolT);
-    val below_def = Logic.mk_equals (belowC newT,
-      Abs ("x", newT, Abs ("y", newT, belowC oldT $ (RepC $ Bound 1) $ (RepC $ Bound 0))));
-
-    fun make_po tac thy1 =
+    fun cpodef_result nonempty admissible thy =
       let
-        val ((_, {type_definition, set_def, ...}), thy2) = thy1
-          |> Typedef.add_typedef def (SOME name) (t, vs, mx) set opt_morphs tac;
-        val lthy3 = thy2
-          |> Theory_Target.instantiation ([full_tname], lhs_tfrees, @{sort po});
-        val below_def' = Syntax.check_term lthy3 below_def;
-        val ((_, (_, below_definition')), lthy4) = lthy3
-          |> Specification.definition (NONE,
-              ((Binding.prefix_name "below_" (Binding.suffix_name "_def" name), []), below_def'));
-        val ctxt_thy = ProofContext.init (ProofContext.theory_of lthy4);
-        val below_definition = singleton (ProofContext.export lthy4 ctxt_thy) below_definition';
-        val thy5 = lthy4
-          |> Class.prove_instantiation_instance
-              (K (Tactic.rtac (@{thm typedef_po} OF [type_definition, below_definition]) 1))
-          |> LocalTheory.exit_global;
-      in ((type_definition, below_definition, set_def), thy5) end;
-
-    fun make_cpo admissible (type_def, below_def, set_def) theory =
-      let
-        (* FIXME fold_rule might fold user input inintentionally *)
-        val admissible' = fold_rule (the_list set_def) admissible;
-        val cpo_thms = map (Thm.transfer theory) [type_def, below_def, admissible'];
-        val theory' = theory
-          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo})
-            (Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1);
-        val cpo_thms' = map (Thm.transfer theory') cpo_thms;
+        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+          |> add_podef def (SOME name) typ set opt_morphs (Tactic.rtac nonempty 1);
+        val (cpo_info, thy3) = thy2
+          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
       in
-        theory'
-        |> Sign.add_path (Binding.name_of name)
-        |> PureThy.add_thms
-          ([((Binding.prefix_name "adm_" name, admissible'), []),
-            ((Binding.prefix_name "cont_" Rep_name, @{thm typedef_cont_Rep} OF cpo_thms'), []),
-            ((Binding.prefix_name "cont_" Abs_name, @{thm typedef_cont_Abs} OF cpo_thms'), []),
-            ((Binding.prefix_name "lub_" name, @{thm typedef_lub} OF cpo_thms'), []),
-            ((Binding.prefix_name "thelub_" name, @{thm typedef_thelub} OF cpo_thms'), []),
-            ((Binding.prefix_name "compact_" name, @{thm typedef_compact} OF cpo_thms'), [])])
-        |> snd
-        |> Sign.parent_path
+        ((info, cpo_info), thy3)
       end;
-
-    fun make_pcpo UU_mem (type_def, below_def, set_def) theory =
-      let
-        (* FIXME fold_rule might fold user input inintentionally *)
-        val UU_mem' = fold_rule (the_list set_def) UU_mem;
-        val pcpo_thms = map (Thm.transfer theory) [type_def, below_def, UU_mem'];
-        val theory' = theory
-          |> AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo})
-            (Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1);
-        val pcpo_thms' = map (Thm.transfer theory') pcpo_thms;
-      in
-        theory'
-        |> Sign.add_path (Binding.name_of name)
-        |> PureThy.add_thms
-          ([((Binding.suffix_name "_strict" Rep_name, @{thm typedef_Rep_strict} OF pcpo_thms'), []),
-            ((Binding.suffix_name "_strict" Abs_name, @{thm typedef_Abs_strict} OF pcpo_thms'), []),
-            ((Binding.suffix_name "_strict_iff" Rep_name, @{thm typedef_Rep_strict_iff} OF pcpo_thms'), []),
-            ((Binding.suffix_name "_strict_iff" Abs_name, @{thm typedef_Abs_strict_iff} OF pcpo_thms'), []),
-            ((Binding.suffix_name "_defined" Rep_name, @{thm typedef_Rep_defined} OF pcpo_thms'), []),
-            ((Binding.suffix_name "_defined" Abs_name, @{thm typedef_Abs_defined} OF pcpo_thms'), [])])
-        |> snd
-        |> Sign.parent_path
-      end;
-
-    fun pcpodef_result UU_mem admissible =
-      make_po (Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1)
-      #-> (fn defs => make_cpo admissible defs #> make_pcpo UU_mem defs);
-
-    fun cpodef_result nonempty admissible =
-      make_po (Tactic.rtac nonempty 1)
-      #-> make_cpo admissible;
   in
-    if pcpo
-    then (goal_UU_mem, goal_admissible, pcpodef_result)
-    else (goal_nonempty, goal_admissible, cpodef_result)
+    (goal_nonempty, goal_admissible, cpodef_result)
   end
   handle ERROR msg =>
     cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name));
 
+fun prepare_pcpodef
+      (prep_term: Proof.context -> 'a -> term)
+      (def: bool)
+      (name: binding)
+      (typ: binding * string list * mixfix)
+      (raw_set: 'a)
+      (opt_morphs: (binding * binding) option)
+      (thy: theory)
+    : term * term * (thm -> thm -> theory -> (Typedef.info * cpo_info * pcpo_info) * theory) =
+  let
+    val (newT, oldT, set, morphs as (Rep_name, Abs_name), lhs_sorts) =
+      prepare prep_term def name typ raw_set opt_morphs thy;
+
+    val goal_UU_mem =
+      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (@{const_name UU}, oldT), set));
+
+    val goal_admissible =
+      HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)));
+
+    fun pcpodef_result UU_mem admissible thy =
+      let
+        val tac = Tactic.rtac exI 1 THEN Tactic.rtac UU_mem 1;
+        val ((info as {type_definition, set_def, ...}, below_def), thy2) = thy
+          |> add_podef def (SOME name) typ set opt_morphs tac;
+        val (cpo_info, thy3) = thy2
+          |> prove_cpo name newT morphs type_definition set_def below_def admissible;
+        val (pcpo_info, thy4) = thy3
+          |> prove_pcpo name newT morphs type_definition set_def below_def UU_mem;
+      in
+        ((info, cpo_info, pcpo_info), thy4)
+      end;
+  in
+    (goal_UU_mem, goal_admissible, pcpodef_result)
+  end
+  handle ERROR msg =>
+    cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name));
+
+
+(* tactic interface *)
+
+fun add_cpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val (goal1, goal2, cpodef_result) =
+      prepare_cpodef Syntax.check_term def name typ set opt_morphs thy;
+    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+  in cpodef_result thm1 thm2 thy end;
+
+fun add_pcpodef def opt_name typ set opt_morphs (tac1, tac2) thy =
+  let
+    val name = the_default (#1 typ) opt_name;
+    val (goal1, goal2, pcpodef_result) =
+      prepare_pcpodef Syntax.check_term def name typ set opt_morphs thy;
+    val thm1 = Goal.prove_global thy [] [] goal1 (K tac1)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove non-emptiness of " ^ quote (Syntax.string_of_term_global thy set));
+    val thm2 = Goal.prove_global thy [] [] goal2 (K tac2)
+      handle ERROR msg => cat_error msg
+        ("Failed to prove admissibility of " ^ quote (Syntax.string_of_term_global thy set));
+  in pcpodef_result thm1 thm2 thy end;
+
 
 (* proof interface *)
 
 local
 
-fun gen_pcpodef_proof prep_term pcpo ((def, name), typ, set, opt_morphs) thy =
+fun gen_cpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
   let
     val (goal1, goal2, make_result) =
-      prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
-    fun after_qed [[th1, th2]] = ProofContext.theory (make_result th1 th2);
+      prepare_cpodef prep_term def name typ set opt_morphs thy;
+    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
+  in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
+
+fun gen_pcpodef_proof prep_term ((def, name), typ, set, opt_morphs) thy =
+  let
+    val (goal1, goal2, make_result) =
+      prepare_pcpodef prep_term def name typ set opt_morphs thy;
+    fun after_qed [[th1, th2]] = ProofContext.theory (snd o make_result th1 th2);
   in Proof.theorem_i NONE after_qed [[(goal1, []), (goal2, [])]] (ProofContext.init thy) end;
 
 in
 
-fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term true x;
-fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term true x;
+fun cpodef_proof x = gen_cpodef_proof Syntax.check_term x;
+fun cpodef_proof_cmd x = gen_cpodef_proof Syntax.read_term x;
 
-fun cpodef_proof x = gen_pcpodef_proof Syntax.check_term false x;
-fun cpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term false x;
+fun pcpodef_proof x = gen_pcpodef_proof Syntax.check_term x;
+fun pcpodef_proof_cmd x = gen_pcpodef_proof Syntax.read_term x;
 
 end;
 
diff -r abf780db30ea -r c6dde2106128 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/General/markup.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -14,7 +14,6 @@
   val name: string -> T -> T
   val bindingN: string val binding: string -> T
   val kindN: string
-  val internalK: string
   val entityN: string val entity: string -> T
   val defN: string
   val refN: string
@@ -154,8 +153,6 @@
 
 val kindN = "kind";
 
-val internalK = "internal";
-
 
 (* formal entities *)
 
diff -r abf780db30ea -r c6dde2106128 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/expression.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -682,7 +682,7 @@
           val (_, thy'') =
             thy'
             |> Sign.mandatory_path (Binding.name_of abinding)
-            |> PureThy.note_thmss Thm.internalK
+            |> PureThy.note_thmss ""
               [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
             ||> Sign.restore_naming thy';
           in (SOME statement, SOME intro, axioms, thy'') end;
@@ -696,7 +696,7 @@
           val (_, thy'''') =
             thy'''
             |> Sign.mandatory_path (Binding.name_of binding)
-            |> PureThy.note_thmss Thm.internalK
+            |> PureThy.note_thmss ""
                  [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
                   ((Binding.conceal (Binding.name axiomsN), []),
                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
@@ -713,7 +713,7 @@
       fold_map (fn (a, spec) => fn axs =>
           let val (ps, qs) = chop (length spec) axs
           in ((a, [(ps, [])]), qs) end) asms axms
-      |> apfst (curry Notes Thm.assumptionK)
+      |> apfst (curry Notes "")
   | assumes_to_notes e axms = (e, axms);
 
 fun defines_to_notes thy (Defines defs) =
@@ -755,7 +755,7 @@
 
     val notes =
       if is_some asm then
-        [(Thm.internalK, [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
+        [("", [((Binding.conceal (Binding.suffix_name ("_" ^ axiomsN) binding), []),
           [([Assumption.assume (cterm_of thy' (the asm))],
             [(Attrib.internal o K) Locale.witness_add])])])]
       else [];
diff -r abf780db30ea -r c6dde2106128 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/locale.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -518,7 +518,7 @@
 
 fun add_decls add loc decl =
   ProofContext.theory ((change_locale loc o apfst o apfst) (add (decl, stamp ()))) #>
-  add_thmss loc Thm.internalK
+  add_thmss loc ""
     [((Binding.conceal Binding.empty, [Attrib.internal (decl_attrib decl)]),
       [([Drule.dummy_thm], [])])];
 
diff -r abf780db30ea -r c6dde2106128 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/proof_context.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -1126,7 +1126,7 @@
   in
     ctxt2
     |> auto_bind_facts (flat propss)
-    |> note_thmss Thm.assumptionK (map fst args ~~ map (map (fn th => ([th], []))) premss)
+    |> note_thmss "" (map fst args ~~ map (map (fn th => ([th], []))) premss)
   end;
 
 in
diff -r abf780db30ea -r c6dde2106128 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/proof_display.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -91,7 +91,7 @@
 in
 
 fun print_results do_print ctxt ((kind, name), facts) =
-  if not do_print orelse kind = "" orelse kind = Thm.internalK then ()
+  if not do_print orelse kind = "" then ()
   else if name = "" then
     Pretty.writeln (Pretty.block (Pretty.str kind :: Pretty.brk 1 :: pretty_facts ctxt facts))
   else Pretty.writeln
diff -r abf780db30ea -r c6dde2106128 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Isar/specification.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -172,7 +172,7 @@
         #>> (fn ths => ((b, atts), [(map Drule.standard' ths, [])])));
 
     (*facts*)
-    val (facts, thy') = axioms_thy |> PureThy.note_thmss Thm.axiomK
+    val (facts, thy') = axioms_thy |> PureThy.note_thmss ""
       (Attrib.map_facts (Attrib.attribute_i axioms_thy) axioms);
 
     val _ =
@@ -329,8 +329,9 @@
         val (facts, goal_ctxt) = elems_ctxt
           |> (snd o ProofContext.add_fixes [(Binding.name Auto_Bind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (obtains ~~ propp)
-          |-> (fn ths => ProofContext.note_thmss Thm.assumptionK
-                [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
+          |-> (fn ths =>
+            ProofContext.note_thmss "" [((Binding.name Obtain.thatN, []), [(ths, [])])] #>
+            #2 #> pair ths);
       in ((prems, stmt, SOME facts), goal_ctxt) end);
 
 structure TheoremHook = Generic_Data
@@ -372,8 +373,7 @@
       end;
   in
     goal_ctxt
-    |> ProofContext.note_thmss Thm.assumptionK
-      [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
+    |> ProofContext.note_thmss "" [((Binding.name Auto_Bind.assmsN, []), [(prems, [])])]
     |> snd
     |> Proof.theorem_i before_qed after_qed' (map snd stmt)
     |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
diff -r abf780db30ea -r c6dde2106128 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/Thy/thm_deps.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -79,9 +79,7 @@
           NONE => I
         | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
     val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
-      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
-        (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
-      then
+      if not concealed andalso is_unused (a, th) then
         (case group of
            NONE => ((a, th) :: thms, grps')
          | SOME grp =>
diff -r abf780db30ea -r c6dde2106128 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/drule.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -710,13 +710,11 @@
 
 val protectI =
   store_thm (Binding.conceal (Binding.name "protectI"))
-    (Thm.kind_rule Thm.internalK (standard
-      (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A))));
+    (standard (Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A)));
 
 val protectD =
   store_thm (Binding.conceal (Binding.name "protectD"))
-    (Thm.kind_rule Thm.internalK (standard
-      (Thm.equal_elim prop_def (Thm.assume (protect A)))));
+    (standard (Thm.equal_elim prop_def (Thm.assume (protect A))));
 
 val protect_cong =
   store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
@@ -734,8 +732,7 @@
 
 val termI =
   store_thm (Binding.conceal (Binding.name "termI"))
-    (Thm.kind_rule Thm.internalK (standard
-      (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)))));
+    (standard (Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A))));
 
 fun mk_term ct =
   let
@@ -764,15 +761,14 @@
 
 val sort_constraintI =
   store_thm (Binding.conceal (Binding.name "sort_constraintI"))
-    (Thm.kind_rule Thm.internalK (standard
-      (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T))));
+    (standard (Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T)));
 
 val sort_constraint_eq =
   store_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
-    (Thm.kind_rule Thm.internalK (standard
+    (standard
       (Thm.equal_intr
         (Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA) (Thm.unvarify sort_constraintI)))
-        (implies_intr_list [A, C] (Thm.assume A)))));
+        (implies_intr_list [A, C] (Thm.assume A))));
 
 end;
 
diff -r abf780db30ea -r c6dde2106128 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Fri Nov 13 11:33:33 2009 +0000
+++ b/src/Pure/more_thm.ML	Fri Nov 13 11:34:05 2009 +0000
@@ -84,14 +84,11 @@
   val has_name_hint: thm -> bool
   val get_name_hint: thm -> string
   val put_name_hint: string -> thm -> thm
-  val axiomK: string
-  val assumptionK: string
   val definitionK: string
   val theoremK: string
   val generatedK : string
   val lemmaK: string
   val corollaryK: string
-  val internalK: string
   val get_kind: thm -> string
   val kind_rule: string -> thm -> thm
   val kind: string -> attribute
@@ -414,14 +411,11 @@
 
 (* theorem kinds *)
 
-val axiomK = "axiom";
-val assumptionK = "assumption";
 val definitionK = "definition";
 val theoremK = "theorem";
 val generatedK = "generatedK"
 val lemmaK = "lemma";
 val corollaryK = "corollary";
-val internalK = Markup.internalK;
 
 fun get_kind thm = the_default "" (Properties.get (Thm.get_tags thm) Markup.kindN);