# HG changeset patch
# User huffman
# Date 1229491133 28800
# Node ID fd8bb7527f7bee017a79357614f582fe0e666e51
# Parent  685c9e05a6ab2c2204ac466cf2586ef759865f3d# Parent  4c243e6a71b27e2cb50909cc5c53d470fa3ac569
merged.

diff -r 685c9e05a6ab -r fd8bb7527f7b Admin/isatest/settings/at-mac-poly-5.1-para
--- a/Admin/isatest/settings/at-mac-poly-5.1-para	Tue Dec 16 09:44:59 2008 -0800
+++ b/Admin/isatest/settings/at-mac-poly-5.1-para	Tue Dec 16 21:18:53 2008 -0800
@@ -4,7 +4,7 @@
   ML_SYSTEM="polyml-5.2.1"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
-  ML_OPTIONS="-H 2000"
+  ML_OPTIONS="--immutable 800 --mutable 1200"
 
 
 ISABELLE_HOME_USER=~/isabelle-at-mac-poly-e
diff -r 685c9e05a6ab -r fd8bb7527f7b NEWS
--- a/NEWS	Tue Dec 16 09:44:59 2008 -0800
+++ b/NEWS	Tue Dec 16 21:18:53 2008 -0800
@@ -239,6 +239,9 @@
 mechanisms may be specified (currently, [SML], [code] or [nbe]).  See
 further src/HOL/ex/Eval_Examples.thy.
 
+* New method "sizechange" to automate termination proofs using (a
+modification of) the size-change principle. Requires SAT solver.
+
 * HOL/Orderings: class "wellorder" moved here, with explicit induction
 rule "less_induct" as assumption.  For instantiation of "wellorder" by
 means of predicate "wf", use rule wf_wellorderI.  INCOMPATIBILITY.
diff -r 685c9e05a6ab -r fd8bb7527f7b doc-src/IsarAdvanced/Classes/style.sty
--- a/doc-src/IsarAdvanced/Classes/style.sty	Tue Dec 16 09:44:59 2008 -0800
+++ b/doc-src/IsarAdvanced/Classes/style.sty	Tue Dec 16 21:18:53 2008 -0800
@@ -30,7 +30,7 @@
 
 \pagestyle{headings}
 \binperiod
-\underscoreon
+\underscoreoff
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
diff -r 685c9e05a6ab -r fd8bb7527f7b doc-src/IsarAdvanced/Codegen/style.sty
--- a/doc-src/IsarAdvanced/Codegen/style.sty	Tue Dec 16 09:44:59 2008 -0800
+++ b/doc-src/IsarAdvanced/Codegen/style.sty	Tue Dec 16 21:18:53 2008 -0800
@@ -42,7 +42,7 @@
 
 \pagestyle{headings}
 \binperiod
-\underscoreon
+\underscoreoff
 
 \renewcommand{\isadigit}[1]{\isamath{#1}}
 
diff -r 685c9e05a6ab -r fd8bb7527f7b doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -804,12 +804,15 @@
     @{command_def (HOL) "print_atps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "atp_info"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{command_def (HOL) "atp_kill"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
+    @{command_def (HOL) "atp_messages"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{method_def (HOL) metis} & : & @{text method} \\
   \end{matharray}
 
   \begin{rail}
   'sledgehammer' (nameref *)
   ;
+  'atp\_messages' ('(' nat ')')?
+  ;
 
   'metis' thmrefs
   ;
@@ -842,6 +845,12 @@
   \item @{command (HOL) atp_kill} terminates all presently running
   provers.
 
+  \item @{command (HOL) atp_messages} displays recent messages issued
+  by automated theorem provers.  This allows to examine results that
+  might have got lost due to the asynchronous nature of default
+  @{command (HOL) sledgehammer} output.  An optional message limit may
+  be specified (default 5).
+
   \item @{method (HOL) metis}~@{text "facts"} invokes the Metis prover
   with the given facts.  Metis is an automated proof tool of medium
   strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r 685c9e05a6ab -r fd8bb7527f7b doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Dec 16 09:44:59 2008 -0800
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Tue Dec 16 21:18:53 2008 -0800
@@ -814,12 +814,15 @@
     \indexdef{HOL}{command}{print\_atps}\hypertarget{command.HOL.print-atps}{\hyperlink{command.HOL.print-atps}{\mbox{\isa{\isacommand{print{\isacharunderscore}atps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{command}{atp\_info}\hypertarget{command.HOL.atp-info}{\hyperlink{command.HOL.atp-info}{\mbox{\isa{\isacommand{atp{\isacharunderscore}info}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{command}{atp\_kill}\hypertarget{command.HOL.atp-kill}{\hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
+    \indexdef{HOL}{command}{atp\_messages}\hypertarget{command.HOL.atp-messages}{\hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}any\ {\isasymrightarrow}{\isachardoublequote}} \\
     \indexdef{HOL}{method}{metis}\hypertarget{method.HOL.metis}{\hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}} & : & \isa{method} \\
   \end{matharray}
 
   \begin{rail}
   'sledgehammer' (nameref *)
   ;
+  'atp\_messages' ('(' nat ')')?
+  ;
 
   'metis' thmrefs
   ;
@@ -850,6 +853,12 @@
   \item \hyperlink{command.HOL.atp-kill}{\mbox{\isa{\isacommand{atp{\isacharunderscore}kill}}}} terminates all presently running
   provers.
 
+  \item \hyperlink{command.HOL.atp-messages}{\mbox{\isa{\isacommand{atp{\isacharunderscore}messages}}}} displays recent messages issued
+  by automated theorem provers.  This allows to examine results that
+  might have got lost due to the asynchronous nature of default
+  \hyperlink{command.HOL.sledgehammer}{\mbox{\isa{\isacommand{sledgehammer}}}} output.  An optional message limit may
+  be specified (default 5).
+
   \item \hyperlink{method.HOL.metis}{\mbox{\isa{metis}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} invokes the Metis prover
   with the given facts.  Metis is an automated proof tool of medium
   strength, but is fully integrated into Isabelle/HOL, with explicit
diff -r 685c9e05a6ab -r fd8bb7527f7b etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Dec 16 09:44:59 2008 -0800
+++ b/etc/isar-keywords-ZF.el	Tue Dec 16 21:18:53 2008 -0800
@@ -200,7 +200,6 @@
     "use"
     "use_thy"
     "using"
-    "value"
     "welcome"
     "with"
     "{"
@@ -323,7 +322,6 @@
     "typ"
     "unused_thms"
     "use_thy"
-    "value"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
diff -r 685c9e05a6ab -r fd8bb7527f7b etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Dec 16 09:44:59 2008 -0800
+++ b/etc/isar-keywords.el	Tue Dec 16 21:18:53 2008 -0800
@@ -32,6 +32,7 @@
     "atom_decl"
     "atp_info"
     "atp_kill"
+    "atp_messages"
     "automaton"
     "ax_specification"
     "axclass"
@@ -331,6 +332,7 @@
     "ML_val"
     "atp_info"
     "atp_kill"
+    "atp_messages"
     "cd"
     "class_deps"
     "code_deps"
diff -r 685c9e05a6ab -r fd8bb7527f7b lib/Tools/usedir
--- a/lib/Tools/usedir	Tue Dec 16 09:44:59 2008 -0800
+++ b/lib/Tools/usedir	Tue Dec 16 21:18:53 2008 -0800
@@ -40,6 +40,11 @@
   echo "  ISABELLE_USEDIR_OPTIONS=$ISABELLE_USEDIR_OPTIONS"
   echo "  HOL_USEDIR_OPTIONS=$HOL_USEDIR_OPTIONS"
   echo
+  echo "  ML_PLATFORM=$ML_PLATFORM"
+  echo "  ML_HOME=$ML_HOME"
+  echo "  ML_SYSTEM=$ML_SYSTEM"
+  echo "  ML_OPTIONS=$ML_OPTIONS"
+  echo
   exit 1
 }
 
diff -r 685c9e05a6ab -r fd8bb7527f7b lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Tue Dec 16 09:44:59 2008 -0800
+++ b/lib/jedit/isabelle.xml	Tue Dec 16 21:18:53 2008 -0800
@@ -56,6 +56,7 @@
       <OPERATOR>atom_decl</OPERATOR>
       <LABEL>atp_info</LABEL>
       <LABEL>atp_kill</LABEL>
+      <LABEL>atp_messages</LABEL>
       <KEYWORD4>attach</KEYWORD4>
       <OPERATOR>automaton</OPERATOR>
       <KEYWORD4>avoids</KEYWORD4>
@@ -154,7 +155,6 @@
       <KEYWORD4>if</KEYWORD4>
       <KEYWORD4>imports</KEYWORD4>
       <KEYWORD4>in</KEYWORD4>
-      <KEYWORD4>includes</KEYWORD4>
       <KEYWORD4>induction</KEYWORD4>
       <OPERATOR>inductive</OPERATOR>
       <KEYWORD1>inductive_cases</KEYWORD1>
@@ -286,6 +286,7 @@
       <OPERATOR>statespace</OPERATOR>
       <KEYWORD4>structure</KEYWORD4>
       <OPERATOR>subclass</OPERATOR>
+      <OPERATOR>sublocale</OPERATOR>
       <OPERATOR>subsect</OPERATOR>
       <OPERATOR>subsection</OPERATOR>
       <OPERATOR>subsubsect</OPERATOR>
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Code_Setup.thy
--- a/src/HOL/Code_Setup.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Code_Setup.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -198,6 +198,10 @@
 
 subsection {* Evaluation and normalization by evaluation *}
 
+setup {*
+  Value.add_evaluator ("SML", Codegen.eval_term o ProofContext.theory_of)
+*}
+
 ML {*
 structure Eval_Method =
 struct
@@ -240,6 +244,10 @@
 
 subsection {* Quickcheck *}
 
+setup {*
+  Quickcheck.add_generator ("SML", Codegen.test_term)
+*}
+
 quickcheck_params [size = 5, iterations = 50]
 
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Divides.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -127,7 +127,7 @@
   note that ultimately show thesis by blast
 qed
 
-lemma dvd_eq_mod_eq_0 [code]: "a dvd b \<longleftrightarrow> b mod a = 0"
+lemma dvd_eq_mod_eq_0 [code unfold]: "a dvd b \<longleftrightarrow> b mod a = 0"
 proof
   assume "b mod a = 0"
   with mod_div_equality [of b a] have "b div a * a = b" by simp
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/FunDef.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -3,11 +3,13 @@
     Author:     Alexander Krauss, TU Muenchen
 *)
 
-header {* General recursive function definitions *}
+header {* Function Definitions and Termination Proofs *}
 
 theory FunDef
 imports Wellfounded
 uses
+  "Tools/prop_logic.ML"
+  "Tools/sat_solver.ML"
   ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/fundef_common.ML")
   ("Tools/function_package/inductive_wrap.ML")
@@ -22,9 +24,14 @@
   ("Tools/function_package/lexicographic_order.ML")
   ("Tools/function_package/fundef_datatype.ML")
   ("Tools/function_package/induction_scheme.ML")
+  ("Tools/function_package/termination.ML")
+  ("Tools/function_package/decompose.ML")
+  ("Tools/function_package/descent.ML")
+  ("Tools/function_package/scnp_solve.ML")
+  ("Tools/function_package/scnp_reconstruct.ML")
 begin
 
-text {* Definitions with default value. *}
+subsection {* Definitions with default value. *}
 
 definition
   THE_default :: "'a \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a" where
@@ -97,9 +104,6 @@
   "wf R \<Longrightarrow> wfP (in_rel R)"
   by (simp add: wfP_def)
 
-inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
-where is_measure_trivial: "is_measure f"
-
 use "Tools/function_package/fundef_lib.ML"
 use "Tools/function_package/fundef_common.ML"
 use "Tools/function_package/inductive_wrap.ML"
@@ -110,19 +114,37 @@
 use "Tools/function_package/pattern_split.ML"
 use "Tools/function_package/auto_term.ML"
 use "Tools/function_package/fundef_package.ML"
-use "Tools/function_package/measure_functions.ML"
-use "Tools/function_package/lexicographic_order.ML"
 use "Tools/function_package/fundef_datatype.ML"
 use "Tools/function_package/induction_scheme.ML"
 
 setup {* 
   FundefPackage.setup 
+  #> FundefDatatype.setup
   #> InductionScheme.setup
-  #> MeasureFunctions.setup
-  #> LexicographicOrder.setup 
-  #> FundefDatatype.setup
 *}
 
+subsection {* Measure Functions *}
+
+inductive is_measure :: "('a \<Rightarrow> nat) \<Rightarrow> bool"
+where is_measure_trivial: "is_measure f"
+
+use "Tools/function_package/measure_functions.ML"
+setup MeasureFunctions.setup
+
+lemma measure_size[measure_function]: "is_measure size"
+by (rule is_measure_trivial)
+
+lemma measure_fst[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
+by (rule is_measure_trivial)
+lemma measure_snd[measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
+by (rule is_measure_trivial)
+
+use "Tools/function_package/lexicographic_order.ML"
+setup LexicographicOrder.setup 
+
+
+subsection {* Congruence Rules *}
+
 lemma let_cong [fundef_cong]:
   "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   unfolding Let_def by blast
@@ -140,17 +162,7 @@
   "f (g x) = f' (g' x') \<Longrightarrow> (f o g) x = (f' o g') x'"
   unfolding o_apply .
 
-subsection {* Setup for termination proofs *}
-
-text {* Rules for generating measure functions *}
-
-lemma [measure_function]: "is_measure size"
-by (rule is_measure_trivial)
-
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (fst p))"
-by (rule is_measure_trivial)
-lemma [measure_function]: "is_measure f \<Longrightarrow> is_measure (\<lambda>p. f (snd p))"
-by (rule is_measure_trivial)
+subsection {* Simp rules for termination proofs *}
 
 lemma termination_basic_simps[termination_simp]:
   "x < (y::nat) \<Longrightarrow> x < y + z" 
@@ -166,5 +178,150 @@
   "prod_size f g p = f (fst p) + g (snd p) + Suc 0"
 by (induct p) auto
 
+subsection {* Decomposition *}
+
+lemma less_by_empty: 
+  "A = {} \<Longrightarrow> A \<subseteq> B"
+and  union_comp_emptyL:
+  "\<lbrakk> A O C = {}; B O C = {} \<rbrakk> \<Longrightarrow> (A \<union> B) O C = {}"
+and union_comp_emptyR:
+  "\<lbrakk> A O B = {}; A O C = {} \<rbrakk> \<Longrightarrow> A O (B \<union> C) = {}"
+and wf_no_loop: 
+  "R O R = {} \<Longrightarrow> wf R"
+by (auto simp add: wf_comp_self[of R])
+
+
+subsection {* Reduction Pairs *}
+
+definition
+  "reduction_pair P = (wf (fst P) \<and> snd P O fst P \<subseteq> fst P)"
+
+lemma reduction_pairI[intro]: "wf R \<Longrightarrow> S O R \<subseteq> R \<Longrightarrow> reduction_pair (R, S)"
+unfolding reduction_pair_def by auto
+
+lemma reduction_pair_lemma:
+  assumes rp: "reduction_pair P"
+  assumes "R \<subseteq> fst P"
+  assumes "S \<subseteq> snd P"
+  assumes "wf S"
+  shows "wf (R \<union> S)"
+proof -
+  from rp `S \<subseteq> snd P` have "wf (fst P)" "S O fst P \<subseteq> fst P"
+    unfolding reduction_pair_def by auto
+  with `wf S` have "wf (fst P \<union> S)" 
+    by (auto intro: wf_union_compatible)
+  moreover from `R \<subseteq> fst P` have "R \<union> S \<subseteq> fst P \<union> S" by auto
+  ultimately show ?thesis by (rule wf_subset) 
+qed
+
+definition
+  "rp_inv_image = (\<lambda>(R,S) f. (inv_image R f, inv_image S f))"
+
+lemma rp_inv_image_rp:
+  "reduction_pair P \<Longrightarrow> reduction_pair (rp_inv_image P f)"
+  unfolding reduction_pair_def rp_inv_image_def split_def
+  by force
+
+
+subsection {* Concrete orders for SCNP termination proofs *}
+
+definition "pair_less = less_than <*lex*> less_than"
+definition "pair_leq = pair_less^="
+definition "max_strict = max_ext pair_less"
+definition "max_weak = max_ext pair_leq \<union> {({}, {})}"
+definition "min_strict = min_ext pair_less"
+definition "min_weak = min_ext pair_leq \<union> {({}, {})}"
+
+lemma wf_pair_less[simp]: "wf pair_less"
+  by (auto simp: pair_less_def)
+
+text {* Introduction rules for @{text pair_less}/@{text pair_leq} *}
+lemma pair_leqI1: "a < b \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+  and pair_leqI2: "a \<le> b \<Longrightarrow> s \<le> t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_leq"
+  and pair_lessI1: "a < b  \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+  and pair_lessI2: "a \<le> b \<Longrightarrow> s < t \<Longrightarrow> ((a, s), (b, t)) \<in> pair_less"
+  unfolding pair_leq_def pair_less_def by auto
+
+text {* Introduction rules for max *}
+lemma smax_emptyI: 
+  "finite Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> ({}, Y) \<in> max_strict" 
+  and smax_insertI: 
+  "\<lbrakk>y \<in> Y; (x, y) \<in> pair_less; (X, Y) \<in> max_strict\<rbrakk> \<Longrightarrow> (insert x X, Y) \<in> max_strict"
+  and wmax_emptyI: 
+  "finite X \<Longrightarrow> ({}, X) \<in> max_weak" 
+  and wmax_insertI:
+  "\<lbrakk>y \<in> YS; (x, y) \<in> pair_leq; (XS, YS) \<in> max_weak\<rbrakk> \<Longrightarrow> (insert x XS, YS) \<in> max_weak" 
+unfolding max_strict_def max_weak_def by (auto elim!: max_ext.cases)
+
+text {* Introduction rules for min *}
+lemma smin_emptyI: 
+  "X \<noteq> {} \<Longrightarrow> (X, {}) \<in> min_strict" 
+  and smin_insertI: 
+  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_less; (XS, YS) \<in> min_strict\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_strict"
+  and wmin_emptyI: 
+  "(X, {}) \<in> min_weak" 
+  and wmin_insertI: 
+  "\<lbrakk>x \<in> XS; (x, y) \<in> pair_leq; (XS, YS) \<in> min_weak\<rbrakk> \<Longrightarrow> (XS, insert y YS) \<in> min_weak" 
+by (auto simp: min_strict_def min_weak_def min_ext_def)
+
+text {* Reduction Pairs *}
+
+lemma max_ext_compat: 
+  assumes "S O R \<subseteq> R"
+  shows "(max_ext S \<union> {({},{})}) O max_ext R \<subseteq> max_ext R"
+using assms 
+apply auto
+apply (elim max_ext.cases)
+apply rule
+apply auto[3]
+apply (drule_tac x=xa in meta_spec)
+apply simp
+apply (erule bexE)
+apply (drule_tac x=xb in meta_spec)
+by auto
+
+lemma max_rpair_set: "reduction_pair (max_strict, max_weak)"
+  unfolding max_strict_def max_weak_def 
+apply (intro reduction_pairI max_ext_wf)
+apply simp
+apply (rule max_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+lemma min_ext_compat: 
+  assumes "S O R \<subseteq> R"
+  shows "(min_ext S \<union> {({},{})}) O min_ext R \<subseteq> min_ext R"
+using assms 
+apply (auto simp: min_ext_def)
+apply (drule_tac x=ya in bspec, assumption)
+apply (erule bexE)
+apply (drule_tac x=xc in bspec)
+apply assumption
+by auto
+
+lemma min_rpair_set: "reduction_pair (min_strict, min_weak)"
+  unfolding min_strict_def min_weak_def 
+apply (intro reduction_pairI min_ext_wf)
+apply simp
+apply (rule min_ext_compat)
+by (auto simp: pair_less_def pair_leq_def)
+
+
+subsection {* Tool setup *}
+
+use "Tools/function_package/termination.ML"
+use "Tools/function_package/decompose.ML"
+use "Tools/function_package/descent.ML"
+use "Tools/function_package/scnp_solve.ML"
+use "Tools/function_package/scnp_reconstruct.ML"
+
+setup {* ScnpReconstruct.setup *}
+(*
+setup {*
+  Context.theory_map (FundefCommon.set_termination_prover (ScnpReconstruct.decomp_scnp 
+  [ScnpSolve.MAX, ScnpSolve.MIN, ScnpSolve.MS])) 
+*}
+*)
+
+
 
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/HOL.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -26,6 +26,7 @@
   "~~/src/Tools/atomize_elim.ML"
   "~~/src/Tools/induct.ML"
   ("~~/src/Tools/induct_tacs.ML")
+  "~~/src/Tools/value.ML"
   "~~/src/Tools/code/code_name.ML"
   "~~/src/Tools/code/code_funcgr.ML"
   "~~/src/Tools/code/code_thingol.ML"
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/IsaMakefile	Tue Dec 16 21:18:53 2008 -0800
@@ -112,6 +112,8 @@
   Tools/dseq.ML \
   Tools/function_package/auto_term.ML \
   Tools/function_package/context_tree.ML \
+  Tools/function_package/decompose.ML \
+  Tools/function_package/descent.ML \
   Tools/function_package/fundef_common.ML \
   Tools/function_package/fundef_core.ML \
   Tools/function_package/fundef_datatype.ML \
@@ -123,8 +125,11 @@
   Tools/function_package/measure_functions.ML \
   Tools/function_package/mutual.ML \
   Tools/function_package/pattern_split.ML \
+  Tools/function_package/scnp_reconstruct.ML \
+  Tools/function_package/scnp_solve.ML \
   Tools/function_package/size.ML \
   Tools/function_package/sum_tree.ML \
+  Tools/function_package/termination.ML \
   Tools/hologic.ML \
   Tools/inductive_codegen.ML \
   Tools/inductive_package.ML \
@@ -179,6 +184,7 @@
   $(SRC)/Tools/code/code_thingol.ML \
   $(SRC)/Tools/induct.ML \
   $(SRC)/Tools/induct_tacs.ML \
+  $(SRC)/Tools/value.ML \
   $(SRC)/Tools/nbe.ML \
   $(SRC)/Tools/random_word.ML \
   $(SRC)/Tools/rat.ML
@@ -776,6 +782,7 @@
   ex/Coherent.thy ex/Dense_Linear_Order_Ex.thy ex/Eval_Examples.thy	\
   ex/Groebner_Examples.thy ex/Random.thy ex/Quickcheck.thy		\
   ex/Codegenerator.thy ex/Codegenerator_Pretty.thy			\
+  ex/CodegenSML_Test.thy 						\
   ex/Commutative_RingEx.thy ex/Efficient_Nat_examples.thy		\
   ex/Hex_Bin_Examples.thy ex/Commutative_Ring_Complete.thy		\
   ex/ExecutableContent.thy ex/Fundefs.thy ex/Guess.thy ex/Hebrew.thy	\
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Library/Executable_Set.thy
--- a/src/HOL/Library/Executable_Set.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Library/Executable_Set.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -28,6 +28,10 @@
 lemma [code]: "eq_set A B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A"
   unfolding eq_set_def by auto
 
+(* FIXME allow for Stefan's code generator:
+declare set_eq_subset[code unfold]
+*)
+
 lemma [code]:
   "a \<in> A \<longleftrightarrow> (\<exists>x\<in>A. x = a)"
   unfolding bex_triv_one_point1 ..
@@ -35,6 +39,8 @@
 definition filter_set :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a set" where
   "filter_set P xs = {x\<in>xs. P x}"
 
+declare filter_set_def[symmetric, code unfold] 
+
 
 subsection {* Operations on lists *}
 
@@ -269,5 +275,6 @@
   Ball ("{*Blall*}")
   Bex ("{*Blex*}")
   filter_set ("{*filter*}")
+  fold ("{* foldl o flip *}")
 
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Library/Multiset.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1481,4 +1481,155 @@
   @{term "{#x+x|x:#M. x<c#}"}.
 *}
 
+
+subsection {* Termination proofs with multiset orders *}
+
+lemma multi_member_skip: "x \<in># XS \<Longrightarrow> x \<in># {# y #} + XS"
+  and multi_member_this: "x \<in># {# x #} + XS"
+  and multi_member_last: "x \<in># {# x #}"
+  by auto
+
+definition "ms_strict = mult pair_less"
+definition "ms_weak = ms_strict \<union> Id"
+
+lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
+unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def
+by (auto intro: wf_mult1 wf_trancl simp: mult_def)
+
+lemma smsI:
+  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z + B) \<in> ms_strict"
+  unfolding ms_strict_def
+by (rule one_step_implies_mult) (auto simp add: max_strict_def pair_less_def elim!:max_ext.cases)
+
+lemma wmsI:
+  "(set_of A, set_of B) \<in> max_strict \<or> A = {#} \<and> B = {#}
+  \<Longrightarrow> (Z + A, Z + B) \<in> ms_weak"
+unfolding ms_weak_def ms_strict_def
+by (auto simp add: pair_less_def max_strict_def elim!:max_ext.cases intro: one_step_implies_mult)
+
+inductive pw_leq
+where
+  pw_leq_empty: "pw_leq {#} {#}"
+| pw_leq_step:  "\<lbrakk>(x,y) \<in> pair_leq; pw_leq X Y \<rbrakk> \<Longrightarrow> pw_leq ({#x#} + X) ({#y#} + Y)"
+
+lemma pw_leq_lstep:
+  "(x, y) \<in> pair_leq \<Longrightarrow> pw_leq {#x#} {#y#}"
+by (drule pw_leq_step) (rule pw_leq_empty, simp)
+
+lemma pw_leq_split:
+  assumes "pw_leq X Y"
+  shows "\<exists>A B Z. X = A + Z \<and> Y = B + Z \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+  using assms
+proof (induct)
+  case pw_leq_empty thus ?case by auto
+next
+  case (pw_leq_step x y X Y)
+  then obtain A B Z where
+    [simp]: "X = A + Z" "Y = B + Z" 
+      and 1[simp]: "(set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#})" 
+    by auto
+  from pw_leq_step have "x = y \<or> (x, y) \<in> pair_less" 
+    unfolding pair_leq_def by auto
+  thus ?case
+  proof
+    assume [simp]: "x = y"
+    have
+      "{#x#} + X = A + ({#y#}+Z) 
+      \<and> {#y#} + Y = B + ({#y#}+Z)
+      \<and> ((set_of A, set_of B) \<in> max_strict \<or> (B = {#} \<and> A = {#}))"
+      by (auto simp: add_ac)
+    thus ?case by (intro exI)
+  next
+    assume A: "(x, y) \<in> pair_less"
+    let ?A' = "{#x#} + A" and ?B' = "{#y#} + B"
+    have "{#x#} + X = ?A' + Z"
+      "{#y#} + Y = ?B' + Z"
+      by (auto simp add: add_ac)
+    moreover have 
+      "(set_of ?A', set_of ?B') \<in> max_strict"
+      using 1 A unfolding max_strict_def 
+      by (auto elim!: max_ext.cases)
+    ultimately show ?thesis by blast
+  qed
+qed
+
+lemma 
+  assumes pwleq: "pw_leq Z Z'"
+  shows ms_strictI: "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_strict"
+  and   ms_weakI1:  "(set_of A, set_of B) \<in> max_strict \<Longrightarrow> (Z + A, Z' + B) \<in> ms_weak"
+  and   ms_weakI2:  "(Z + {#}, Z' + {#}) \<in> ms_weak"
+proof -
+  from pw_leq_split[OF pwleq] 
+  obtain A' B' Z''
+    where [simp]: "Z = A' + Z''" "Z' = B' + Z''"
+    and mx_or_empty: "(set_of A', set_of B') \<in> max_strict \<or> (A' = {#} \<and> B' = {#})"
+    by blast
+  {
+    assume max: "(set_of A, set_of B) \<in> max_strict"
+    from mx_or_empty
+    have "(Z'' + (A + A'), Z'' + (B + B')) \<in> ms_strict"
+    proof
+      assume max': "(set_of A', set_of B') \<in> max_strict"
+      with max have "(set_of (A + A'), set_of (B + B')) \<in> max_strict"
+        by (auto simp: max_strict_def intro: max_ext_additive)
+      thus ?thesis by (rule smsI) 
+    next
+      assume [simp]: "A' = {#} \<and> B' = {#}"
+      show ?thesis by (rule smsI) (auto intro: max)
+    qed
+    thus "(Z + A, Z' + B) \<in> ms_strict" by (simp add:add_ac)
+    thus "(Z + A, Z' + B) \<in> ms_weak" by (simp add: ms_weak_def)
+  }
+  from mx_or_empty
+  have "(Z'' + A', Z'' + B') \<in> ms_weak" by (rule wmsI)
+  thus "(Z + {#}, Z' + {#}) \<in> ms_weak" by (simp add:add_ac)
+qed
+
+lemma empty_idemp: "{#} + x = x" "x + {#} = x"
+and nonempty_plus: "{# x #} + rs \<noteq> {#}"
+and nonempty_single: "{# x #} \<noteq> {#}"
+by auto
+
+setup {*
+let
+  fun msetT T = Type ("Multiset.multiset", [T]);
+
+  fun mk_mset T [] = Const (@{const_name Mempty}, msetT T)
+    | mk_mset T [x] = Const (@{const_name single}, T --> msetT T) $ x
+    | mk_mset T (x :: xs) =
+          Const (@{const_name plus}, msetT T --> msetT T --> msetT T) $
+                mk_mset T [x] $ mk_mset T xs
+
+  fun mset_member_tac m i =
+      (if m <= 0 then
+           rtac @{thm multi_member_this} i ORELSE rtac @{thm multi_member_last} i
+       else
+           rtac @{thm multi_member_skip} i THEN mset_member_tac (m - 1) i)
+
+  val mset_nonempty_tac =
+      rtac @{thm nonempty_plus} ORELSE' rtac @{thm nonempty_single}
+
+  val regroup_munion_conv =
+      FundefLib.regroup_conv @{const_name Multiset.Mempty} @{const_name plus}
+        (map (fn t => t RS eq_reflection) (@{thms union_ac} @ @{thms empty_idemp}))
+
+  fun unfold_pwleq_tac i =
+    (rtac @{thm pw_leq_step} i THEN (fn st => unfold_pwleq_tac (i + 1) st))
+      ORELSE (rtac @{thm pw_leq_lstep} i)
+      ORELSE (rtac @{thm pw_leq_empty} i)
+
+  val set_of_simps = [@{thm set_of_empty}, @{thm set_of_single}, @{thm set_of_union},
+                      @{thm Un_insert_left}, @{thm Un_empty_left}]
+in
+  ScnpReconstruct.multiset_setup (ScnpReconstruct.Multiset 
+  {
+    msetT=msetT, mk_mset=mk_mset, mset_regroup_conv=regroup_munion_conv,
+    mset_member_tac=mset_member_tac, mset_nonempty_tac=mset_nonempty_tac,
+    mset_pwleq_tac=unfold_pwleq_tac, set_of_simps=set_of_simps,
+    smsI'=@{thm ms_strictI}, wmsI2''=@{thm ms_weakI2}, wmsI1=@{thm ms_weakI1},
+    reduction_pair=@{thm ms_reduction_pair}
+  })
 end
+*}
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory CK_Machine 
   imports "../Nominal" 
 begin
@@ -41,21 +39,21 @@
 
 section {* Capture-Avoiding Substitution *}
 
-consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
-
 nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+where
   "(VAR x)[y::=s] = (if x=y then s else (VAR x))"
-  "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
-  "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])"
-  "(NUM n)[y::=s] = NUM n"
-  "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
-  "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
-  "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
-  "TRUE[y::=s] = TRUE"
-  "FALSE[y::=s] = FALSE"
-  "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
-  "(ZET t)[y::=s] = ZET (t[y::=s])"
-  "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])"
+| "(APP t\<^isub>1 t\<^isub>2)[y::=s] = APP (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+| "x\<sharp>(y,s) \<Longrightarrow> (LAM [x].t)[y::=s] = LAM [x].(t[y::=s])"
+| "(NUM n)[y::=s] = NUM n"
+| "(t\<^isub>1 -- t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) -- (t\<^isub>2[y::=s])"
+| "(t\<^isub>1 ++ t\<^isub>2)[y::=s] = (t\<^isub>1[y::=s]) ++ (t\<^isub>2[y::=s])"
+| "x\<sharp>(y,s) \<Longrightarrow> (FIX [x].t)[y::=s] = FIX [x].(t[y::=s])"
+| "TRUE[y::=s] = TRUE"
+| "FALSE[y::=s] = FALSE"
+| "(IF t1 t2 t3)[y::=s] = IF (t1[y::=s]) (t2[y::=s]) (t3[y::=s])"
+| "(ZET t)[y::=s] = ZET (t[y::=s])"
+| "(EQI t1 t2)[y::=s] = EQI (t1[y::=s]) (t2[y::=s])"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/CR_Takahashi.thy
--- a/src/HOL/Nominal/Examples/CR_Takahashi.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/CR_Takahashi.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 (* Authors: Christian Urban and Mathilde Arnaud                   *)
 (*                                                                *)
 (* A formalisation of the Church-Rosser proof by Masako Takahashi.*)
@@ -20,12 +18,12 @@
   | App "lam" "lam"
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
-consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
-
 nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+where
   "(Var x)[y::=s] = (if x=y then s else (Var x))"
-  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
-  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
+| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)
@@ -54,14 +52,16 @@
 lemma substitution_lemma:  
   assumes a: "x\<noteq>y" "x\<sharp>u"
   shows "t[x::=s][y::=u] = t[y::=u][x::=s[y::=u]]"
-using a by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
-           (auto simp add: fresh_fact forget)
+using a 
+by (nominal_induct t avoiding: x y s u rule: lam.strong_induct)
+   (auto simp add: fresh_fact forget)
 
 lemma subst_rename: 
   assumes a: "y\<sharp>t"
   shows "t[x::=s] = ([(y,x)]\<bullet>t)[y::=s]"
-using a by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
-           (auto simp add: calc_atm fresh_atm abs_fresh)
+using a 
+by (nominal_induct t avoiding: x y s rule: lam.strong_induct)
+   (auto simp add: swap_simps fresh_atm abs_fresh)
 
 section {* Beta-Reduction *}
 
@@ -103,8 +103,9 @@
 lemma One_subst: 
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
   shows "t1[x::=s1] \<longrightarrow>\<^isub>1 t2[x::=s2]" 
-using a by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
-           (auto simp add: substitution_lemma fresh_atm fresh_fact)
+using a 
+by (nominal_induct t1 t2 avoiding: s1 s2 x rule: One.strong_induct)
+   (auto simp add: substitution_lemma fresh_atm fresh_fact)
 
 lemma better_o4_intro:
   assumes a: "t1 \<longrightarrow>\<^isub>1 t2" "s1 \<longrightarrow>\<^isub>1 s2"
@@ -202,35 +203,30 @@
 by (nominal_induct M rule: lam.strong_induct)
    (auto dest!: Dev_Lam intro: better_d4_intro)
 
-(* needs fixing *)
 lemma Triangle:
   assumes a: "t \<longrightarrow>\<^isub>d t1" "t \<longrightarrow>\<^isub>1 t2"
   shows "t2 \<longrightarrow>\<^isub>1 t1"
 using a 
 proof(nominal_induct avoiding: t2 rule: Dev.strong_induct)
   case (d4 x s1 s2 t1 t1' t2) 
-  have ih1: "\<And>t. t1 \<longrightarrow>\<^isub>1 t \<Longrightarrow>  t \<longrightarrow>\<^isub>1 t1'"
-  and  ih2: "\<And>s. s1 \<longrightarrow>\<^isub>1 s \<Longrightarrow>  s \<longrightarrow>\<^isub>1 s2"
-  and  fc: "x\<sharp>t2" "x\<sharp>s1" "x\<sharp>s2" by fact+ 
+  have  fc: "x\<sharp>t2" "x\<sharp>s1" by fact+ 
   have "App (Lam [x].t1) s1 \<longrightarrow>\<^isub>1 t2" by fact
-  then obtain t' s' where "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
-                           (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
+  then obtain t' s' where reds: 
+             "(t2 = App (Lam [x].t') s' \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s') \<or> 
+              (t2 = t'[x::=s'] \<and> t1 \<longrightarrow>\<^isub>1 t' \<and> s1 \<longrightarrow>\<^isub>1 s')"
   using fc by (auto dest!: One_Redex)
-  then show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]"
-    apply -
-    apply(erule disjE)
-    apply(erule conjE)+
-    apply(simp)
-    apply(rule o4)
-    using fc apply(simp)
-    using ih1 apply(simp)
-    using ih2 apply(simp)
-    apply(erule conjE)+
-    apply(simp)
-    apply(rule One_subst)
-    using ih1 apply(simp)
-    using ih2 apply(simp)    
-    done
+  have ih1: "t1 \<longrightarrow>\<^isub>1 t' \<Longrightarrow>  t' \<longrightarrow>\<^isub>1 t1'" by fact
+  have ih2: "s1 \<longrightarrow>\<^isub>1 s' \<Longrightarrow>  s' \<longrightarrow>\<^isub>1 s2" by fact
+  { assume "t1 \<longrightarrow>\<^isub>1 t'" "s1 \<longrightarrow>\<^isub>1 s'"
+    then have "App (Lam [x].t') s' \<longrightarrow>\<^isub>1 t1'[x::=s2]" 
+      using ih1 ih2 by (auto intro: better_o4_intro)
+  }
+  moreover
+  { assume "t1 \<longrightarrow>\<^isub>1 t'" "s1 \<longrightarrow>\<^isub>1 s'"
+    then have "t'[x::=s'] \<longrightarrow>\<^isub>1 t1'[x::=s2]" 
+      using ih1 ih2 by (auto intro: One_subst)
+  }
+  ultimately show "t2 \<longrightarrow>\<^isub>1 t1'[x::=s2]" using reds by auto 
 qed (auto dest!: One_Lam One_Var One_App)
 
 lemma Diamond_for_One:
@@ -310,4 +306,6 @@
   then show "\<exists>t3. t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3 \<and> t2 \<longrightarrow>\<^isub>\<beta>\<^sup>* t3" by (simp add: Beta_star_equals_One_star)
 qed
 
+
+
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Class.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Class
 imports "../Nominal" 
 begin
@@ -17,16 +15,22 @@
   | OR   "ty" "ty"   ("_ OR _" [100,100] 100)
   | IMP  "ty" "ty"   ("_ IMP _" [100,100] 100)
 
-instance ty :: size ..
-
-nominal_primrec
+instantiation ty :: size
+begin
+
+nominal_primrec size_ty
+where
   "size (PR s)     = (1::nat)"
-  "size (NOT T)     = 1 + size T"
-  "size (T1 AND T2) = 1 + size T1 + size T2"
-  "size (T1 OR T2)  = 1 + size T1 + size T2"
-  "size (T1 IMP T2) = 1 + size T1 + size T2"
+| "size (NOT T)     = 1 + size T"
+| "size (T1 AND T2) = 1 + size T1 + size T2"
+| "size (T1 OR T2)  = 1 + size T1 + size T2"
+| "size (T1 IMP T2) = 1 + size T1 + size T2"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ty_cases:
   fixes T::ty
   shows "(\<exists>s. T=PR s) \<or> (\<exists>T'. T=NOT T') \<or> (\<exists>S U. T=S OR U) \<or> (\<exists>S U. T=S AND U) \<or> (\<exists>S U. T=S IMP U)"
@@ -66,25 +70,23 @@
 
 text {* renaming functions *}
 
-consts
-  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
+nominal_primrec (freshness_context: "(d::coname,e::coname)") 
   crename :: "trm \<Rightarrow> coname \<Rightarrow> coname \<Rightarrow> trm"  ("_[_\<turnstile>c>_]" [100,100,100] 100) 
-
-nominal_primrec (freshness_context: "(d::coname,e::coname)") 
+where
   "(Ax x a)[d\<turnstile>c>e] = (if a=d then Ax x e else Ax x a)" 
-  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" 
-  "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" 
-  "a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
-  "\<lbrakk>a\<sharp>(d,e,N,c);b\<sharp>(d,e,M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] = 
+| "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>M\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[d\<turnstile>c>e] = Cut <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e])" 
+| "(NotR (x).M a)[d\<turnstile>c>e] = (if a=d then NotR (x).(M[d\<turnstile>c>e]) e else NotR (x).(M[d\<turnstile>c>e]) a)" 
+| "a\<sharp>(d,e) \<Longrightarrow> (NotL <a>.M x)[d\<turnstile>c>e] = (NotL <a>.(M[d\<turnstile>c>e]) x)" 
+| "\<lbrakk>a\<sharp>(d,e,N,c);b\<sharp>(d,e,M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[d\<turnstile>c>e] = 
           (if c=d then AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d \<turnstile>c>e]) e else AndR <a>.(M[d\<turnstile>c>e]) <b>.(N[d\<turnstile>c>e]) c)" 
-  "x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
-  "x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
-  "a\<sharp>(d,e,b) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)"
-  "a\<sharp>(d,e,b) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
-  "\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
-  "a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
+| "x\<sharp>y \<Longrightarrow> (AndL1 (x).M y)[d\<turnstile>c>e] = AndL1 (x).(M[d\<turnstile>c>e]) y"
+| "x\<sharp>y \<Longrightarrow> (AndL2 (x).M y)[d\<turnstile>c>e] = AndL2 (x).(M[d\<turnstile>c>e]) y"
+| "a\<sharp>(d,e,b) \<Longrightarrow> (OrR1 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR1 <a>.(M[d\<turnstile>c>e]) e else OrR1 <a>.(M[d\<turnstile>c>e]) b)"
+| "a\<sharp>(d,e,b) \<Longrightarrow> (OrR2 <a>.M b)[d\<turnstile>c>e] = (if b=d then OrR2 <a>.(M[d\<turnstile>c>e]) e else OrR2 <a>.(M[d\<turnstile>c>e]) b)"
+| "\<lbrakk>x\<sharp>(N,z);y\<sharp>(M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[d\<turnstile>c>e] = OrL (x).(M[d\<turnstile>c>e]) (y).(N[d\<turnstile>c>e]) z"
+| "a\<sharp>(d,e,b) \<Longrightarrow> (ImpR (x).<a>.M b)[d\<turnstile>c>e] = 
        (if b=d then ImpR (x).<a>.(M[d\<turnstile>c>e]) e else ImpR (x).<a>.(M[d\<turnstile>c>e]) b)"
-  "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
+| "\<lbrakk>a\<sharp>(d,e,N);x\<sharp>(M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[d\<turnstile>c>e] = ImpL <a>.(M[d\<turnstile>c>e]) (x).(N[d\<turnstile>c>e]) y"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -92,19 +94,21 @@
 done
 
 nominal_primrec (freshness_context: "(u::name,v::name)") 
+  nrename :: "trm \<Rightarrow> name \<Rightarrow> name \<Rightarrow> trm"      ("_[_\<turnstile>n>_]" [100,100,100] 100) 
+where
   "(Ax x a)[u\<turnstile>n>v] = (if x=u then Ax v a else Ax x a)" 
-  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
-  "x\<sharp>(u,v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" 
-  "(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)" 
-  "\<lbrakk>a\<sharp>(N,c);b\<sharp>(M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" 
-  "x\<sharp>(u,v,y) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)"
-  "x\<sharp>(u,v,y) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)"
-  "a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
-  "a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
-  "\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = 
+| "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N)[u\<turnstile>n>v] = Cut <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v])" 
+| "x\<sharp>(u,v) \<Longrightarrow> (NotR (x).M a)[u\<turnstile>n>v] = NotR (x).(M[u\<turnstile>n>v]) a" 
+| "(NotL <a>.M x)[u\<turnstile>n>v] = (if x=u then NotL <a>.(M[u\<turnstile>n>v]) v else NotL <a>.(M[u\<turnstile>n>v]) x)" 
+| "\<lbrakk>a\<sharp>(N,c);b\<sharp>(M,c);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c)[u\<turnstile>n>v] = AndR <a>.(M[u\<turnstile>n>v]) <b>.(N[u\<turnstile>n>v]) c" 
+| "x\<sharp>(u,v,y) \<Longrightarrow> (AndL1 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL1 (x).(M[u\<turnstile>n>v]) v else AndL1 (x).(M[u\<turnstile>n>v]) y)"
+| "x\<sharp>(u,v,y) \<Longrightarrow> (AndL2 (x).M y)[u\<turnstile>n>v] = (if y=u then AndL2 (x).(M[u\<turnstile>n>v]) v else AndL2 (x).(M[u\<turnstile>n>v]) y)"
+| "a\<sharp>b \<Longrightarrow> (OrR1 <a>.M b)[u\<turnstile>n>v] = OrR1 <a>.(M[u\<turnstile>n>v]) b"
+| "a\<sharp>b \<Longrightarrow> (OrR2 <a>.M b)[u\<turnstile>n>v] = OrR2 <a>.(M[u\<turnstile>n>v]) b"
+| "\<lbrakk>x\<sharp>(u,v,N,z);y\<sharp>(u,v,M,z);y\<noteq>x\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N z)[u\<turnstile>n>v] = 
         (if z=u then OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) v else OrL (x).(M[u\<turnstile>n>v]) (y).(N[u\<turnstile>n>v]) z)"
-  "\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
-  "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
+| "\<lbrakk>a\<sharp>b; x\<sharp>(u,v)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b)[u\<turnstile>n>v] = ImpR (x).<a>.(M[u\<turnstile>n>v]) b"
+| "\<lbrakk>a\<sharp>N;x\<sharp>(u,v,M,y)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y)[u\<turnstile>n>v] = 
         (if y=u then ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) v else ImpL <a>.(M[u\<turnstile>n>v]) (x).(N[u\<turnstile>n>v]) y)"
 apply(finite_guess)+
 apply(rule TrueI)+
@@ -766,32 +770,30 @@
 apply(simp add: fin_supp)
 done
 
-consts
+nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
   substn :: "trm \<Rightarrow> name   \<Rightarrow> coname \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=<_>._}" [100,100,100,100] 100) 
-  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)
-
-nominal_primrec (freshness_context: "(y::name,c::coname,P::trm)")
+where
   "(Ax x a){y:=<c>.P} = (if x=y then Cut <c>.P (y).Ax y a else Ax x a)" 
-  "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
+| "\<lbrakk>a\<sharp>(c,P,N);x\<sharp>(y,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){y:=<c>.P} = 
   (if M=Ax y a then Cut <c>.P (x).(N{y:=<c>.P}) else Cut <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}))" 
-  "x\<sharp>(y,P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
-  "a\<sharp>(c,P) \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
+| "x\<sharp>(y,P) \<Longrightarrow> (NotR (x).M a){y:=<c>.P} = NotR (x).(M{y:=<c>.P}) a" 
+| "a\<sharp>(c,P) \<Longrightarrow> (NotL <a>.M x){y:=<c>.P} = 
   (if x=y then fresh_fun (\<lambda>x'. Cut <c>.P (x').NotL <a>.(M{y:=<c>.P}) x') else NotL <a>.(M{y:=<c>.P}) x)"
-  "\<lbrakk>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> 
+| "\<lbrakk>a\<sharp>(c,P,N,d);b\<sharp>(c,P,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> 
   (AndR <a>.M <b>.N d){y:=<c>.P} = AndR <a>.(M{y:=<c>.P}) <b>.(N{y:=<c>.P}) d" 
-  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL1 (x).M z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(M{y:=<c>.P}) z') 
    else AndL1 (x).(M{y:=<c>.P}) z)"
-  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(M{y:=<c>.P}) z') 
    else AndL2 (x).(M{y:=<c>.P}) z)"
-  "a\<sharp>(c,P,b) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
-  "a\<sharp>(c,P,b) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
-  "\<lbrakk>x\<sharp>(y,N,P,z);u\<sharp>(y,M,P,z);x\<noteq>u\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
+| "a\<sharp>(c,P,b) \<Longrightarrow> (OrR1 <a>.M b){y:=<c>.P} = OrR1 <a>.(M{y:=<c>.P}) b"
+| "a\<sharp>(c,P,b) \<Longrightarrow> (OrR2 <a>.M b){y:=<c>.P} = OrR2 <a>.(M{y:=<c>.P}) b"
+| "\<lbrakk>x\<sharp>(y,N,P,z);u\<sharp>(y,M,P,z);x\<noteq>u\<rbrakk> \<Longrightarrow> (OrL (x).M (u).N z){y:=<c>.P} = 
   (if z=y then fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z') 
    else OrL (x).(M{y:=<c>.P}) (u).(N{y:=<c>.P}) z)"
-  "\<lbrakk>a\<sharp>(b,c,P); x\<sharp>(y,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
-  "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
+| "\<lbrakk>a\<sharp>(b,c,P); x\<sharp>(y,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){y:=<c>.P} = ImpR (x).<a>.(M{y:=<c>.P}) b"
+| "\<lbrakk>a\<sharp>(N,c,P);x\<sharp>(y,P,M,z)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N z){y:=<c>.P} = 
   (if y=z then fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z') 
    else ImpL <a>.(M{y:=<c>.P}) (x).(N{y:=<c>.P}) z)"
 apply(finite_guess)+
@@ -842,27 +844,29 @@
 done
 
 nominal_primrec (freshness_context: "(d::name,z::coname,P::trm)")
+  substc :: "trm \<Rightarrow> coname \<Rightarrow> name   \<Rightarrow> trm \<Rightarrow> trm" ("_{_:=(_)._}" [100,100,100,100] 100)
+where
   "(Ax x a){d:=(z).P} = (if d=a then Cut <a>.(Ax x a) (z).P else Ax x a)" 
-  "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(d,P,N);x\<sharp>(z,P,M)\<rbrakk> \<Longrightarrow> (Cut <a>.M (x).N){d:=(z).P} = 
   (if N=Ax x d then Cut <a>.(M{d:=(z).P}) (z).P else Cut <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}))" 
-  "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
+| "x\<sharp>(z,P) \<Longrightarrow> (NotR (x).M a){d:=(z).P} = 
   (if d=a then fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(M{d:=(z).P}) a' (z).P) else NotR (x).(M{d:=(z).P}) a)" 
-  "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
-  "\<lbrakk>a\<sharp>(P,c,N,d);b\<sharp>(P,c,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c){d:=(z).P} = 
+| "a\<sharp>(d,P) \<Longrightarrow> (NotL <a>.M x){d:=(z).P} = NotL <a>.(M{d:=(z).P}) x" 
+| "\<lbrakk>a\<sharp>(P,c,N,d);b\<sharp>(P,c,M,d);b\<noteq>a\<rbrakk> \<Longrightarrow> (AndR <a>.M <b>.N c){d:=(z).P} = 
   (if d=c then fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) a') (z).P)
    else AndR <a>.(M{d:=(z).P}) <b>.(N{d:=(z).P}) c)" 
-  "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
-  "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
-  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
+| "x\<sharp>(y,z,P) \<Longrightarrow> (AndL1 (x).M y){d:=(z).P} = AndL1 (x).(M{d:=(z).P}) y"
+| "x\<sharp>(y,P,z) \<Longrightarrow> (AndL2 (x).M y){d:=(z).P} = AndL2 (x).(M{d:=(z).P}) y"
+| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR1 <a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(M{d:=(z).P}) a' (z).P) else OrR1 <a>.(M{d:=(z).P}) b)"
-  "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
+| "a\<sharp>(d,P,b) \<Longrightarrow> (OrR2 <a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(M{d:=(z).P}) a' (z).P) else OrR2 <a>.(M{d:=(z).P}) b)"
-  "\<lbrakk>x\<sharp>(N,z,P,u);y\<sharp>(M,z,P,u);x\<noteq>y\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N u){d:=(z).P} = 
+| "\<lbrakk>x\<sharp>(N,z,P,u);y\<sharp>(M,z,P,u);x\<noteq>y\<rbrakk> \<Longrightarrow> (OrL (x).M (y).N u){d:=(z).P} = 
   OrL (x).(M{d:=(z).P}) (y).(N{d:=(z).P}) u" 
-  "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(b,d,P); x\<sharp>(z,P)\<rbrakk> \<Longrightarrow> (ImpR (x).<a>.M b){d:=(z).P} = 
   (if d=b then fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(M{d:=(z).P}) a' (z).P) 
    else ImpR (x).<a>.(M{d:=(z).P}) b)"
-  "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
+| "\<lbrakk>a\<sharp>(N,d,P);x\<sharp>(y,z,P,M)\<rbrakk> \<Longrightarrow> (ImpL <a>.M (x).N y){d:=(z).P} = 
   ImpL <a>.(M{d:=(z).P}) (x).(N{d:=(z).P}) y"
 apply(finite_guess)+
 apply(rule TrueI)+
@@ -10305,11 +10309,10 @@
 lemma BINDINGc_decreasing:
   shows "X\<subseteq>Y \<Longrightarrow> BINDINGc B Y \<subseteq> BINDINGc B X"
 by (simp add: BINDINGc_def) (blast) 
-
-consts
-  NOTRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
   
 nominal_primrec
+  NOTRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set"
+where
  "NOTRIGHT (NOT B) X = { <a>:NotR (x).M a | a x M. fic (NotR (x).M a) a \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10365,11 +10368,10 @@
 apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
 apply(simp add: swap_simps)
 done
-
-consts
-  NOTLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
   
 nominal_primrec
+  NOTLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set"
+where
  "NOTLEFT (NOT B) X = { (x):NotL <a>.M x | a x M. fin (NotL <a>.M x) x \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10425,11 +10427,10 @@
 apply(drule pt_bij1[OF pt_coname_inst, OF at_coname_inst])
 apply(simp add: swap_simps)
 done
-
-consts
-  ANDRIGHT::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
   
 nominal_primrec
+  ANDRIGHT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ANDRIGHT (B AND C) X Y = 
             { <c>:AndR <a>.M <b>.N c | c a b M N. fic (AndR <a>.M <b>.N c) c \<and> <a>:M \<in> X \<and> <b>:N \<in> Y }"
 apply(rule TrueI)+
@@ -10505,10 +10506,9 @@
 apply(simp)
 done
 
-consts
-  ANDLEFT1::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  ANDLEFT1 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ANDLEFT1 (B AND C) X = { (y):AndL1 (x).M y | x y M. fin (AndL1 (x).M y) y \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10565,10 +10565,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ANDLEFT2::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  ANDLEFT2 :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ANDLEFT2 (B AND C) X = { (y):AndL2 (x).M y | x y M. fin (AndL2 (x).M y) y \<and> (x):M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10625,10 +10624,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ORLEFT::"ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-  
 nominal_primrec
+  ORLEFT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "ORLEFT (B OR C) X Y = 
             { (z):OrL (x).M (y).N z | x y z M N. fin (OrL (x).M (y).N z) z \<and> (x):M \<in> X \<and> (y):N \<in> Y }"
 apply(rule TrueI)+
@@ -10704,10 +10702,9 @@
 apply(simp add: swap_simps)
 done
 
-consts
-  ORRIGHT1::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  ORRIGHT1 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ORRIGHT1 (B OR C) X = { <b>:OrR1 <a>.M b | a b M. fic (OrR1 <a>.M b) b \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10764,10 +10761,9 @@
 apply(simp)
 done
 
-consts
-  ORRIGHT2::"ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  ORRIGHT2 :: "ty \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "ORRIGHT2 (B OR C) X = { <b>:OrR2 <a>.M b | a b M. fic (OrR2 <a>.M b) b \<and> <a>:M \<in> X }"
 apply(rule TrueI)+
 done
@@ -10824,10 +10820,9 @@
 apply(simp)
 done
 
-consts
-  IMPRIGHT::"ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
-
 nominal_primrec
+  IMPRIGHT :: "ty \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ctrm set \<Rightarrow> ctrm set"
+where
  "IMPRIGHT (B IMP C) X Y Z U= 
         { <b>:ImpR (x).<a>.M b | x a b M. fic (ImpR (x).<a>.M b) b 
                                         \<and> (\<forall>z P. x\<sharp>(z,P) \<and> (z):P \<in> Z \<longrightarrow> (x):(M{a:=(z).P}) \<in> X)
@@ -10954,10 +10949,9 @@
 apply(perm_simp add: nsubst_eqvt fresh_right)
 done
 
-consts
-  IMPLEFT::"ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
-
 nominal_primrec
+  IMPLEFT :: "ty \<Rightarrow> ctrm set \<Rightarrow> ntrm set \<Rightarrow> ntrm set"
+where
  "IMPLEFT (B IMP C) X Y = 
         { (y):ImpL <a>.M (x).N y | x a y M N. fin (ImpL <a>.M (x).N y) y \<and> <a>:M \<in> X \<and> (x):N \<in> Y }"
 apply(rule TrueI)+
@@ -17800,23 +17794,21 @@
 apply(auto)
 done 
 
-consts
+nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
   stn :: "trm\<Rightarrow>(name\<times>coname\<times>trm) list\<Rightarrow>trm" 
-  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
-
-nominal_primrec (freshness_context: "\<theta>n::(name\<times>coname\<times>trm)")
+where
   "stn (Ax x a) \<theta>n = lookupc x a \<theta>n"
-  "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)" 
-  "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
-  "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
-  "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
-  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
-  "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
-  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
-  "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
-  "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
-  "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
+| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,\<theta>n)\<rbrakk> \<Longrightarrow> stn (Cut <a>.M (x).N) \<theta>n = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>n \<Longrightarrow> stn (NotR (x).M a) \<theta>n = (NotR (x).M a)"
+| "a\<sharp>\<theta>n \<Longrightarrow>stn (NotL <a>.M x) \<theta>n = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>n);b\<sharp>(M,d,a,\<theta>n)\<rbrakk> \<Longrightarrow> stn (AndR <a>.M <b>.N d) \<theta>n = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL1 (x).M z) \<theta>n = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>n) \<Longrightarrow> stn (AndL2 (x).M z) \<theta>n = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR1 <a>.M b) \<theta>n = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>n) \<Longrightarrow> stn (OrR2 <a>.M b) \<theta>n = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>n);u\<sharp>(M,z,x,\<theta>n)\<rbrakk> \<Longrightarrow> stn (OrL (x).M (u).N z) \<theta>n = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>n);x\<sharp>\<theta>n\<rbrakk> \<Longrightarrow> stn (ImpR (x).<a>.M b) \<theta>n = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>n);x\<sharp>(M,z,\<theta>n)\<rbrakk> \<Longrightarrow> stn (ImpL <a>.M (x).N z) \<theta>n = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -17824,18 +17816,20 @@
 done
 
 nominal_primrec (freshness_context: "\<theta>c::(coname\<times>name\<times>trm)")
+  stc :: "trm\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm" 
+where
   "stc (Ax x a) \<theta>c = lookupd x a \<theta>c"
-  "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)" 
-  "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
-  "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
-  "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
-  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
-  "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
-  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
-  "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
-  "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
-  "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
+| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,\<theta>c)\<rbrakk> \<Longrightarrow> stc (Cut <a>.M (x).N) \<theta>c = (Cut <a>.M (x).N)" 
+| "x\<sharp>\<theta>c \<Longrightarrow> stc (NotR (x).M a) \<theta>c = (NotR (x).M a)"
+| "a\<sharp>\<theta>c \<Longrightarrow> stc (NotL <a>.M x) \<theta>c = (NotL <a>.M x)"
+| "\<lbrakk>a\<sharp>(N,d,b,\<theta>c);b\<sharp>(M,d,a,\<theta>c)\<rbrakk> \<Longrightarrow> stc (AndR <a>.M <b>.N d) \<theta>c = (AndR <a>.M <b>.N d)"
+| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL1 (x).M z) \<theta>c = (AndL1 (x).M z)"
+| "x\<sharp>(z,\<theta>c) \<Longrightarrow> stc (AndL2 (x).M z) \<theta>c = (AndL2 (x).M z)"
+| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR1 <a>.M b) \<theta>c = (OrR1 <a>.M b)"
+| "a\<sharp>(b,\<theta>c) \<Longrightarrow> stc (OrR2 <a>.M b) \<theta>c = (OrR2 <a>.M b)"
+| "\<lbrakk>x\<sharp>(N,z,u,\<theta>c);u\<sharp>(M,z,x,\<theta>c)\<rbrakk> \<Longrightarrow> stc (OrL (x).M (u).N z) \<theta>c = (OrL (x).M (u).N z)"
+| "\<lbrakk>a\<sharp>(b,\<theta>c);x\<sharp>\<theta>c\<rbrakk> \<Longrightarrow> stc (ImpR (x).<a>.M b) \<theta>c = (ImpR (x).<a>.M b)"
+| "\<lbrakk>a\<sharp>(N,\<theta>c);x\<sharp>(M,z,\<theta>c)\<rbrakk> \<Longrightarrow> stc (ImpL <a>.M (x).N z) \<theta>c = (ImpL <a>.M (x).N z)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh abs_supp fin_supp)+
@@ -17926,51 +17920,50 @@
 apply(perm_simp)
 done
 
-consts
+nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
   psubst :: "(name\<times>coname\<times>trm) list\<Rightarrow>(coname\<times>name\<times>trm) list\<Rightarrow>trm\<Rightarrow>trm" ("_,_<_>" [100,100,100] 100) 
-
-nominal_primrec (freshness_context: "(\<theta>n::(name\<times>coname\<times>trm) list,\<theta>c::(coname\<times>name\<times>trm) list)")
+where
   "\<theta>n,\<theta>c<Ax x a> = lookup x a \<theta>n \<theta>c" 
-  "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> = 
+| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c);x\<sharp>(M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> \<theta>n,\<theta>c<Cut <a>.M (x).N> = 
    Cut <a>.(if \<exists>x. M=Ax x a then stn M \<theta>n else \<theta>n,\<theta>c<M>) 
        (x).(if \<exists>a. N=Ax x a then stc N \<theta>c else \<theta>n,\<theta>c<N>)" 
-  "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
+| "x\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotR (x).M a> = 
   (case (findc \<theta>c a) of 
        Some (u,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.NotR (x).(\<theta>n,\<theta>c<M>) a' (u).P) 
      | None \<Rightarrow> NotR (x).(\<theta>n,\<theta>c<M>) a)"
-  "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
+| "a\<sharp>(\<theta>n,\<theta>c) \<Longrightarrow> \<theta>n,\<theta>c<NotL <a>.M x> = 
   (case (findn \<theta>n x) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>x'. Cut <c>.P (x').(NotL <a>.(\<theta>n,\<theta>c<M>) x')) 
      | None \<Rightarrow> NotL <a>.(\<theta>n,\<theta>c<M>) x)"
-  "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) = 
+| "\<lbrakk>a\<sharp>(N,c,\<theta>n,\<theta>c);b\<sharp>(M,c,\<theta>n,\<theta>c);b\<noteq>a\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<AndR <a>.M <b>.N c>) = 
   (case (findc \<theta>c c) of 
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.(AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) a') (x).P)
      | None \<Rightarrow> AndR <a>.(\<theta>n,\<theta>c<M>) <b>.(\<theta>n,\<theta>c<N>) c)"
-  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
+| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL1 (x).M z>) = 
   (case (findn \<theta>n z) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL1 (x).(\<theta>n,\<theta>c<M>) z') 
      | None \<Rightarrow> AndL1 (x).(\<theta>n,\<theta>c<M>) z)"
-  "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
+| "x\<sharp>(z,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<AndL2 (x).M z>) = 
   (case (findn \<theta>n z) of 
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').AndL2 (x).(\<theta>n,\<theta>c<M>) z') 
      | None \<Rightarrow> AndL2 (x).(\<theta>n,\<theta>c<M>) z)"
-  "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
+| "\<lbrakk>x\<sharp>(N,z,\<theta>n,\<theta>c);u\<sharp>(M,z,\<theta>n,\<theta>c);x\<noteq>u\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<OrL (x).M (u).N z>) =
   (case (findn \<theta>n z) of  
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z') 
      | None \<Rightarrow> OrL (x).(\<theta>n,\<theta>c<M>) (u).(\<theta>n,\<theta>c<N>) z)"
-  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
+| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR1 <a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR1 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
      | None \<Rightarrow> OrR1 <a>.(\<theta>n,\<theta>c<M>) b)"
-  "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
+| "a\<sharp>(b,\<theta>n,\<theta>c) \<Longrightarrow> (\<theta>n,\<theta>c<OrR2 <a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (x,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.OrR2 <a>.(\<theta>n,\<theta>c<M>) a' (x).P) 
      | None \<Rightarrow> OrR2 <a>.(\<theta>n,\<theta>c<M>) b)"
-  "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) = 
+| "\<lbrakk>a\<sharp>(b,\<theta>n,\<theta>c); x\<sharp>(\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpR (x).<a>.M b>) = 
   (case (findc \<theta>c b) of
        Some (z,P) \<Rightarrow> fresh_fun (\<lambda>a'. Cut <a'>.ImpR (x).<a>.(\<theta>n,\<theta>c<M>) a' (z).P)
      | None \<Rightarrow> ImpR (x).<a>.(\<theta>n,\<theta>c<M>) b)"
-  "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) = 
+| "\<lbrakk>a\<sharp>(N,\<theta>n,\<theta>c); x\<sharp>(z,M,\<theta>n,\<theta>c)\<rbrakk> \<Longrightarrow> (\<theta>n,\<theta>c<ImpL <a>.M (x).N z>) = 
   (case (findn \<theta>n z) of
        Some (c,P) \<Rightarrow> fresh_fun (\<lambda>z'. Cut <c>.P (z').ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z') 
      | None \<Rightarrow> ImpL <a>.(\<theta>n,\<theta>c<M>) (x).(\<theta>n,\<theta>c<N>) z)"
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Compile.thy
--- a/src/HOL/Nominal/Examples/Compile.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Compile.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 (* The definitions for a challenge suggested by Adam Chlipala *)
 
 theory Compile
@@ -92,20 +90,24 @@
 
 text {* capture-avoiding substitution *}
 
-consts
-  subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
+class subst =
+  fixes subst :: "'a \<Rightarrow> name \<Rightarrow> 'a \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 
-nominal_primrec
+instantiation trm :: subst
+begin
+
+nominal_primrec subst_trm
+where
   "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
-  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
-  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
-  "(Const n)[y::=t'] = Const n"
-  "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
-  "(Fst e)[y::=t'] = Fst (e[y::=t'])"
-  "(Snd e)[y::=t'] = Snd (e[y::=t'])"
-  "(InL e)[y::=t'] = InL (e[y::=t'])"
-  "(InR e)[y::=t'] = InR (e[y::=t'])"
-  "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
+| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
+| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+| "(Const n)[y::=t'] = Const n"
+| "(Pr e1 e2)[y::=t'] = Pr (e1[y::=t']) (e2[y::=t'])"
+| "(Fst e)[y::=t'] = Fst (e[y::=t'])"
+| "(Snd e)[y::=t'] = Snd (e[y::=t'])"
+| "(InL e)[y::=t'] = InL (e[y::=t'])"
+| "(InR e)[y::=t'] = InR (e[y::=t'])"
+| "\<lbrakk>z\<noteq>x; x\<sharp>y; x\<sharp>e; x\<sharp>e2; z\<sharp>y; z\<sharp>e; z\<sharp>e1; x\<sharp>t'; z\<sharp>t'\<rbrakk> \<Longrightarrow>
      (Case e of inl x \<rightarrow> e1 | inr z \<rightarrow> e2)[y::=t'] =
        (Case (e[y::=t']) of inl x \<rightarrow> (e1[y::=t']) | inr z \<rightarrow> (e2[y::=t']))"
   apply(finite_guess)+
@@ -114,23 +116,35 @@
   apply(fresh_guess)+
   done
 
-nominal_primrec (Isubst)
+instance ..
+
+end
+
+instantiation trmI :: subst
+begin
+
+nominal_primrec subst_trmI
+where
   "(IVar x)[y::=t'] = (if x=y then t' else (IVar x))"
-  "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
-  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
-  "(INat n)[y::=t'] = INat n"
-  "(IUnit)[y::=t'] = IUnit"
-  "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
-  "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
-  "(IRef e)[y::=t'] = IRef (e[y::=t'])"
-  "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
-  "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
+| "(IApp t1 t2)[y::=t'] = IApp (t1[y::=t']) (t2[y::=t'])"
+| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (ILam [x].t)[y::=t'] = ILam [x].(t[y::=t'])"
+| "(INat n)[y::=t'] = INat n"
+| "(IUnit)[y::=t'] = IUnit"
+| "(ISucc e)[y::=t'] = ISucc (e[y::=t'])"
+| "(IAss e1 e2)[y::=t'] = IAss (e1[y::=t']) (e2[y::=t'])"
+| "(IRef e)[y::=t'] = IRef (e[y::=t'])"
+| "(ISeq e1 e2)[y::=t'] = ISeq (e1[y::=t']) (e2[y::=t'])"
+| "(Iif e e1 e2)[y::=t'] = Iif (e[y::=t']) (e1[y::=t']) (e2[y::=t'])"
   apply(finite_guess)+
   apply(rule TrueI)+
   apply(simp add: abs_fresh)+
   apply(fresh_guess)+
   done
 
+instance ..
+
+end
+
 lemma Isubst_eqvt[eqvt]:
   fixes pi::"name prm"
   and   t1::"trmI"
@@ -138,7 +152,7 @@
   and   x::"name"
   shows "pi\<bullet>(t1[x::=t2]) = ((pi\<bullet>t1)[(pi\<bullet>x)::=(pi\<bullet>t2)])"
   apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
-  apply (simp_all add: Isubst.simps eqvts fresh_bij)
+  apply (simp_all add: subst_trmI.simps eqvts fresh_bij)
   done
 
 lemma Isubst_supp:
@@ -147,7 +161,7 @@
   and   x::"name"
   shows "((supp (t1[x::=t2]))::name set) \<subseteq> (supp t2)\<union>((supp t1)-{x})"
   apply (nominal_induct t1 avoiding: x t2 rule: trmI.strong_induct)
-  apply (auto simp add: Isubst.simps trmI.supp supp_atm abs_supp supp_nat)
+  apply (auto simp add: subst_trmI.simps trmI.supp supp_atm abs_supp supp_nat)
   apply blast+
   done
 
@@ -198,29 +212,29 @@
 
 text {* Translation functions *}
 
-consts trans :: "trm \<Rightarrow> trmI" 
-
 nominal_primrec
+  trans :: "trm \<Rightarrow> trmI"
+where
   "trans (Var x) = (IVar x)"
-  "trans (App e1 e2) = IApp (trans e1) (trans e2)"
-  "trans (Lam [x].e) = ILam [x].(trans e)"
-  "trans (Const n) = INat n"
-  "trans (Pr e1 e2) = 
+| "trans (App e1 e2) = IApp (trans e1) (trans e2)"
+| "trans (Lam [x].e) = ILam [x].(trans e)"
+| "trans (Const n) = INat n"
+| "trans (Pr e1 e2) = 
        (let limit = IRef(INat 0) in 
         let v1 = (trans e1) in 
         let v2 = (trans e2) in 
         (((ISucc limit)\<mapsto>v1);;(ISucc(ISucc limit)\<mapsto>v2));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  "trans (Fst e) = IRef (ISucc (trans e))"
-  "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
-  "trans (InL e) = 
+| "trans (Fst e) = IRef (ISucc (trans e))"
+| "trans (Snd e) = IRef (ISucc (ISucc (trans e)))"
+| "trans (InL e) = 
         (let limit = IRef(INat 0) in 
          let v = (trans e) in 
          (((ISucc limit)\<mapsto>INat(0));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  "trans (InR e) = 
+| "trans (InR e) = 
         (let limit = IRef(INat 0) in 
          let v = (trans e) in 
          (((ISucc limit)\<mapsto>INat(1));;(ISucc(ISucc limit)\<mapsto>v));;(INat 0 \<mapsto> ISucc(ISucc(limit))))"
-  "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
+| "\<lbrakk>x2\<noteq>x1; x1\<sharp>e; x1\<sharp>e2; x2\<sharp>e; x2\<sharp>e1\<rbrakk> \<Longrightarrow> 
    trans (Case e of inl x1 \<rightarrow> e1 | inr x2 \<rightarrow> e2) =
        (let v = (trans e) in
         let v1 = (trans e1) in
@@ -232,11 +246,11 @@
   apply(fresh_guess add: Let_def)+
   done
 
-consts trans_type :: "ty \<Rightarrow> tyI"
-
 nominal_primrec
+  trans_type :: "ty \<Rightarrow> tyI"
+where
   "trans_type (Data \<sigma>) = DataI(NatI)"
-  "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
+| "trans_type (\<tau>1\<rightarrow>\<tau>2) = (trans_type \<tau>1)\<rightarrow>(trans_type \<tau>2)"
   by (rule TrueI)+
 
 end
\ No newline at end of file
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Contexts.thy
--- a/src/HOL/Nominal/Examples/Contexts.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Contexts.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Contexts
 imports "../Nominal"
 begin
@@ -42,12 +40,12 @@
 
 text {* Capture-Avoiding Substitution *}
 
-consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
-
 nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
+where
   "(Var x)[y::=s] = (if x=y then s else (Var x))"
-  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
-  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
+| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)
@@ -59,14 +57,13 @@
   This operation is possibly capturing.
 *}
 
-consts 
+nominal_primrec
   filling :: "ctx \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
-
-nominal_primrec
+where
   "\<box>\<lbrakk>t\<rbrakk> = t"
-  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
-  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
-  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
+| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
+| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
+| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
 by (rule TrueI)+
 
 text {* 
@@ -81,14 +78,13 @@
 
 text {* The composition of two contexts. *}
 
-consts 
+nominal_primrec
  ctx_compose :: "ctx \<Rightarrow> ctx \<Rightarrow> ctx" ("_ \<circ> _" [100,100] 100)
-
-nominal_primrec
+where
   "\<box> \<circ> E' = E'"
-  "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
-  "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
-  "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
+| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
+| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
+| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
 by (rule TrueI)+
   
 lemma ctx_compose:
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Crary.thy
--- a/src/HOL/Nominal/Examples/Crary.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Crary.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,4 +1,3 @@
-(* "$Id$" *)
 (*                                                    *)
 (* Formalisation of the chapter on Logical Relations  *)
 (* and a Case Study in Equivalence Checking           *)
@@ -47,14 +46,20 @@
   shows "(\<exists> T\<^isub>1 T\<^isub>2. T=T\<^isub>1\<rightarrow>T\<^isub>2) \<or> T=TUnit \<or> T=TBase"
 by (induct T rule:ty.induct) (auto)
 
-instance ty :: size ..
+instantiation ty :: size
+begin
 
-nominal_primrec
+nominal_primrec size_ty
+where
   "size (TBase) = 1"
-  "size (TUnit) = 1"
-  "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
+| "size (TUnit) = 1"
+| "size (T\<^isub>1\<rightarrow>T\<^isub>2) = size T\<^isub>1 + size T\<^isub>2"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ty_size_greater_zero[simp]:
   fixes T::"ty"
   shows "size T > 0"
@@ -87,16 +92,15 @@
 using a
 by (induct rule: lookup.induct)
    (auto simp add: fresh_list_cons fresh_prod fresh_atm)
-
-consts
-  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
  
 nominal_primrec
+  psubst :: "Subst \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [100,100] 130)
+where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
-  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
-  "\<theta><(Const n)> = Const n"
-  "\<theta><(Unit)> = Unit"
+| "\<theta><(App t\<^isub>1 t\<^isub>2)> = App \<theta><t\<^isub>1> \<theta><t\<^isub>2>"
+| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)"
+| "\<theta><(Const n)> = Const n"
+| "\<theta><(Unit)> = Unit"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Fsub.thy
--- a/src/HOL/Nominal/Examples/Fsub.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Fsub.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 (*<*)
 theory Fsub
 imports "../Nominal" 
@@ -229,32 +227,26 @@
 
 section {* Size and Capture-Avoiding Substitution for Types *}
 
-consts size_ty :: "ty \<Rightarrow> nat"
-
 nominal_primrec
+  size_ty :: "ty \<Rightarrow> nat"
+where
   "size_ty (Tvar X) = 1"
-  "size_ty (Top) = 1"
-  "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
-  "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
+| "size_ty (Top) = 1"
+| "size_ty (T1 \<rightarrow> T2) = (size_ty T1) + (size_ty T2) + 1"
+| "X\<sharp>T1 \<Longrightarrow> size_ty (\<forall>[X<:T1].T2) = (size_ty T1) + (size_ty T2) + 1"
   apply (finite_guess)+
   apply (rule TrueI)+
   apply (simp add: fresh_nat)
   apply (fresh_guess)+
   done
 
-consts subst_ty :: "tyvrs \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> ty"
-
-syntax 
- subst_ty_syn :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
-
-translations 
-  "T1[Y:=T2]\<^isub>t\<^isub>y" \<rightleftharpoons> "subst_ty Y T2 T1"
-
 nominal_primrec
+  subst_ty :: "ty \<Rightarrow> tyvrs \<Rightarrow> ty \<Rightarrow> ty" ("_[_:=_]\<^isub>t\<^isub>y" [100,100,100] 100)
+where
   "(Tvar X)[Y:=T]\<^isub>t\<^isub>y= (if X=Y then T else (Tvar X))"
-  "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
-  "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
-  "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
+| "(Top)[Y:=T]\<^isub>t\<^isub>y = Top"
+| "(T\<^isub>1 \<rightarrow> T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (T\<^isub>1[Y:=T]\<^isub>t\<^isub>y) \<rightarrow> (T\<^isub>2[Y:=T]\<^isub>t\<^isub>y)"
+| "\<lbrakk>X\<sharp>(Y,T); X\<sharp>T\<^isub>1\<rbrakk> \<Longrightarrow> (\<forall>[X<:T\<^isub>1].T\<^isub>2)[Y:=T]\<^isub>t\<^isub>y = (\<forall>[X<:(T\<^isub>1[Y:=T]\<^isub>t\<^isub>y)].(T\<^isub>2[Y:=T]\<^isub>t\<^isub>y))"
   apply (finite_guess)+
   apply (rule TrueI)+
   apply (simp add: abs_fresh)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Height.thy
--- a/src/HOL/Nominal/Examples/Height.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Height.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Height
   imports "../Nominal"
 begin
@@ -17,13 +15,13 @@
   | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
 
 text {* Definition of the height-function on lambda-terms. *} 
-consts 
-  height :: "lam \<Rightarrow> int"
 
 nominal_primrec
+  height :: "lam \<Rightarrow> int"
+where
   "height (Var x) = 1"
-  "height (App t1 t2) = (max (height t1) (height t2)) + 1"
-  "height (Lam [a].t) = (height t) + 1"
+| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
+| "height (Lam [a].t) = (height t) + 1"
   apply(finite_guess add: perm_int_def)+
   apply(rule TrueI)+
   apply(simp add: fresh_int)
@@ -32,13 +30,12 @@
 
 text {* Definition of capture-avoiding substitution. *}
 
-consts
+nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [100,100,100] 100)
-
-nominal_primrec
+where
   "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
-  "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
-  "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
+| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
+| "\<lbrakk>x\<sharp>y; x\<sharp>t'\<rbrakk> \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Lam_Funs.thy
--- a/src/HOL/Nominal/Examples/Lam_Funs.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Lam_Funs.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Lam_Funs
   imports "../Nominal"
 begin
@@ -18,13 +16,12 @@
 
 text {* The depth of a lambda-term. *}
 
-consts 
+nominal_primrec
   depth :: "lam \<Rightarrow> nat"
-
-nominal_primrec
+where
   "depth (Var x) = 1"
-  "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
-  "depth (Lam [a].t) = (depth t) + 1"
+| "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1"
+| "depth (Lam [a].t) = (depth t) + 1"
   apply(finite_guess)+
   apply(rule TrueI)+
   apply(simp add: fresh_nat)
@@ -38,13 +35,12 @@
   the invariant that frees always returns a finite set of names. 
 *}
 
-consts 
+nominal_primrec (invariant: "\<lambda>s::name set. finite s")
   frees :: "lam \<Rightarrow> name set"
-
-nominal_primrec (invariant: "\<lambda>s::name set. finite s")
+where
   "frees (Var a) = {a}"
-  "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
-  "frees (Lam [a].t) = (frees t) - {a}"
+| "frees (App t1 t2) = (frees t1) \<union> (frees t2)"
+| "frees (Lam [a].t) = (frees t) - {a}"
 apply(finite_guess)+
 apply(simp)+ 
 apply(simp add: fresh_def)
@@ -78,14 +74,13 @@
   and   X::"name"
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
-
-consts
-  psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
  
 nominal_primrec
+  psubst :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam"  ("_<_>" [95,95] 105)
+where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
-  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
+| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
+| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
@@ -130,26 +125,24 @@
 
 text {* Filling a lambda-term into a context. *}
 
-consts 
+nominal_primrec
   filling :: "clam \<Rightarrow> lam \<Rightarrow> lam" ("_\<lbrakk>_\<rbrakk>" [100,100] 100)
-
-nominal_primrec
+where
   "\<box>\<lbrakk>t\<rbrakk> = t"
-  "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
-  "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
-  "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
+| "(CAppL E t')\<lbrakk>t\<rbrakk> = App (E\<lbrakk>t\<rbrakk>) t'"
+| "(CAppR t' E)\<lbrakk>t\<rbrakk> = App t' (E\<lbrakk>t\<rbrakk>)"
+| "(CLam [x].E)\<lbrakk>t\<rbrakk> = Lam [x].(E\<lbrakk>t\<rbrakk>)" 
 by (rule TrueI)+
 
 text {* Composition od two contexts *}
 
-consts 
+nominal_primrec
  clam_compose :: "clam \<Rightarrow> clam \<Rightarrow> clam" ("_ \<circ> _" [100,100] 100)
-
-nominal_primrec
+where
   "\<box> \<circ> E' = E'"
-  "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
-  "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
-  "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
+| "(CAppL E t') \<circ> E' = CAppL (E \<circ> E') t'"
+| "(CAppR t' E) \<circ> E' = CAppR t' (E \<circ> E')"
+| "(CLam [x].E) \<circ> E' = CLam [x].(E \<circ> E')"
 by (rule TrueI)+
   
 lemma clam_compose:
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 (* Formalisation of weakening using locally nameless    *)
 (* terms; the nominal infrastructure can also derive    *)
 (* strong induction principles for such representations *)
@@ -29,13 +27,13 @@
 by (induct t rule: llam.induct)
    (auto simp add: llam.inject)
 
-consts llam_size :: "llam \<Rightarrow> nat"
-
 nominal_primrec
- "llam_size (lPar a) = 1"
- "llam_size (lVar n) = 1"
- "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
- "llam_size (lLam t) = 1 + (llam_size t)"
+  llam_size :: "llam \<Rightarrow> nat"
+where
+  "llam_size (lPar a) = 1"
+| "llam_size (lVar n) = 1"
+| "llam_size (lApp t1 t2) = 1 + (llam_size t1) + (llam_size t2)"
+| "llam_size (lLam t) = 1 + (llam_size t)"
 by (rule TrueI)+
 
 function  
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/SN.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory SN
   imports Lam_Funs
 begin
@@ -228,12 +226,11 @@
 
 section {* Candidates *}
 
-consts
+nominal_primrec
   RED :: "ty \<Rightarrow> lam set"
-
-nominal_primrec
+where
   "RED (TVar X) = {t. SN(t)}"
-  "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
+| "RED (\<tau>\<rightarrow>\<sigma>) =   {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"
 by (rule TrueI)+
 
 text {* neutral terms *}
@@ -248,13 +245,12 @@
 where
   fst[intro!]:  "(App t s) \<guillemotright> t"
 
-consts
+nominal_primrec
   fst_app_aux::"lam\<Rightarrow>lam option"
-
-nominal_primrec
+where
   "fst_app_aux (Var a)     = None"
-  "fst_app_aux (App t1 t2) = Some t1"
-  "fst_app_aux (Lam [x].t) = None"
+| "fst_app_aux (App t1 t2) = Some t1"
+| "fst_app_aux (Lam [x].t) = None"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: fresh_none)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/SOS.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,4 +1,3 @@
-(* "$Id$" *)
 (*                                                        *)
 (* Formalisation of some typical SOS-proofs.              *)
 (*                                                        *) 
@@ -62,13 +61,12 @@
 
 (* parallel substitution *)
 
-consts
+nominal_primrec
   psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm"  ("_<_>" [95,95] 105)
- 
-nominal_primrec
+where
   "\<theta><(Var x)> = (lookup \<theta> x)"
-  "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
-  "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
+| "\<theta><(App e\<^isub>1 e\<^isub>2)> = App (\<theta><e\<^isub>1>) (\<theta><e\<^isub>2>)"
+| "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].e)> = Lam [x].(\<theta><e>)"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)+
@@ -349,12 +347,12 @@
 using h by (induct) (auto)
 
 (* Valuation *)
-consts
-  V :: "ty \<Rightarrow> trm set" 
 
 nominal_primrec
+  V :: "ty \<Rightarrow> trm set" 
+where
   "V (TVar x) = {e. val e}"
-  "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
+| "V (T\<^isub>1 \<rightarrow> T\<^isub>2) = {Lam [x].e | x e. \<forall> v \<in> (V T\<^isub>1). \<exists> v'. e[x::=v] \<Down> v' \<and> v' \<in> V T\<^isub>2}"
   by (rule TrueI)+ 
 
 lemma V_eqvt:
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Standardization.thy
--- a/src/HOL/Nominal/Examples/Standardization.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Standardization.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/Examples/Standardization.thy
-    ID:         $Id$
     Author:     Stefan Berghofer and Tobias Nipkow
     Copyright   2005, 2008 TU Muenchen
 *)
@@ -24,24 +23,30 @@
 | App "lam" "lam" (infixl "\<degree>" 200)
 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [0, 10] 10)
 
-instance lam :: size ..
+instantiation lam :: size
+begin
 
-nominal_primrec
+nominal_primrec size_lam
+where
   "size (Var n) = 0"
-  "size (t \<degree> u) = size t + size u + 1"
-  "size (Lam [x].t) = size t + 1"
+| "size (t \<degree> u) = size t + size u + 1"
+| "size (Lam [x].t) = size t + 1"
   apply finite_guess+
   apply (rule TrueI)+
   apply (simp add: fresh_nat)
   apply fresh_guess+
   done
 
-consts subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [300, 0, 0] 300)
+instance ..
+
+end
 
 nominal_primrec
+  subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]" [300, 0, 0] 300)
+where
   subst_Var: "(Var x)[y::=s] = (if x=y then s else (Var x))"
-  subst_App: "(t\<^isub>1 \<degree> t\<^isub>2)[y::=s] = t\<^isub>1[y::=s] \<degree> t\<^isub>2[y::=s]"
-  subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
+| subst_App: "(t\<^isub>1 \<degree> t\<^isub>2)[y::=s] = t\<^isub>1[y::=s] \<degree> t\<^isub>2[y::=s]"
+| subst_Lam: "x \<sharp> (y, s) \<Longrightarrow> (Lam [x].t)[y::=s] = (Lam [x].(t[y::=s]))"
   apply(finite_guess)+
   apply(rule TrueI)+
   apply(simp add: abs_fresh)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/Type_Preservation.thy
--- a/src/HOL/Nominal/Examples/Type_Preservation.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/Type_Preservation.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* $Id$ *)
-
 theory Type_Preservation
   imports Nominal
 begin
@@ -21,13 +19,12 @@
 
 text {* Capture-Avoiding Substitution *}
 
-consts 
+nominal_primrec
   subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam"  ("_[_::=_]")
-
-nominal_primrec
+where
   "(Var x)[y::=s] = (if x=y then s else (Var x))"
-  "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
-  "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
+| "(App t\<^isub>1 t\<^isub>2)[y::=s] = App (t\<^isub>1[y::=s]) (t\<^isub>2[y::=s])"
+| "x\<sharp>(y,s) \<Longrightarrow> (Lam [x].t)[y::=s] = Lam [x].(t[y::=s])"
 apply(finite_guess)+
 apply(rule TrueI)+
 apply(simp add: abs_fresh)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Examples/W.thy
--- a/src/HOL/Nominal/Examples/W.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Examples/W.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,3 @@
-(* "$Id$" *)
-
 theory W
 imports Nominal
 begin
@@ -50,26 +48,68 @@
   Ctxt  = "(var\<times>tyS) list" 
 
 text {* free type variables *}
-consts
-  ftv    :: "'a \<Rightarrow> tvar list"
+
+class ftv = type +
+  fixes ftv :: "'a \<Rightarrow> tvar list"
+
+instantiation * :: (ftv, ftv) ftv
+begin
+
+primrec ftv_prod
+where
+ "ftv (x::'a::ftv, y::'b::ftv) = (ftv x)@(ftv y)"
+
+instance ..
+
+end
 
-primrec (ftv_of_prod)
- "ftv (x,y) = (ftv x)@(ftv y)"
+instantiation tvar :: ftv
+begin
+
+definition
+  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
 
-defs (overloaded)
-  ftv_of_tvar[simp]:  "ftv X \<equiv> [(X::tvar)]"
+instance ..
+
+end
+
+instantiation var :: ftv
+begin
+
+definition
   ftv_of_var[simp]:   "ftv (x::var) \<equiv> []" 
 
-primrec (ftv_of_list)
+instance ..
+
+end
+
+instantiation list :: (ftv) ftv
+begin
+
+primrec ftv_list
+where
   "ftv [] = []"
-  "ftv (x#xs) = (ftv x)@(ftv xs)"
+| "ftv (x#xs) = (ftv x)@(ftv xs)"
+
+instance ..
+
+end
 
 (* free type-variables of types *)
-nominal_primrec (ftv_ty)
+
+instantiation ty :: ftv
+begin
+
+nominal_primrec ftv_ty
+where
   "ftv (TVar X) = [X]"
-  "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
+| "ftv (T\<^isub>1\<rightarrow>T\<^isub>2) = (ftv T\<^isub>1)@(ftv T\<^isub>2)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma ftv_ty_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   T::"ty"
@@ -77,9 +117,13 @@
 by (nominal_induct T rule: ty.strong_induct)
    (perm_simp add: append_eqvt)+
 
-nominal_primrec (ftv_tyS)
+instantiation tyS :: ftv
+begin
+
+nominal_primrec ftv_tyS
+where
   "ftv (Ty T)    = ftv T"
-  "ftv (\<forall>[X].S) = (ftv S) - [X]"
+| "ftv (\<forall>[X].S) = (ftv S) - [X]"
 apply(finite_guess add: ftv_ty_eqvt fs_tvar1)+
 apply(rule TrueI)+
 apply(rule difference_fresh)
@@ -87,6 +131,10 @@
 apply(fresh_guess add: ftv_ty_eqvt fs_tvar1)+
 done
 
+instance ..
+
+end
+
 lemma ftv_tyS_eqvt[eqvt]:
   fixes pi::"tvar prm"
   and   S::"tyS"
@@ -140,11 +188,11 @@
 
 types Subst = "(tvar\<times>ty) list"
 
-consts
- psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
+class psubst =
+  fixes psubst :: "Subst \<Rightarrow> 'a \<Rightarrow> 'a"       ("_<_>" [100,60] 120)
 
 abbreviation 
-  subst :: "'a \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
+  subst :: "'a::psubst \<Rightarrow> tvar \<Rightarrow> ty \<Rightarrow> 'a"  ("_[_::=_]" [100,100,100] 100)
 where
   "smth[X::=T] \<equiv> ([(X,T)])<smth>" 
 
@@ -159,11 +207,19 @@
   shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)"
 by (induct \<theta>) (auto simp add: eqvts)
 
-nominal_primrec (psubst_ty)
+instantiation ty :: psubst
+begin
+
+nominal_primrec psubst_ty
+where
   "\<theta><TVar X>   = lookup \<theta> X"
-  "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
+| "\<theta><T\<^isub>1 \<rightarrow> T\<^isub>2> = (\<theta><T\<^isub>1>) \<rightarrow> (\<theta><T\<^isub>2>)"
 by (rule TrueI)+
 
+instance ..
+
+end
+
 lemma psubst_ty_eqvt[eqvt]:
   fixes pi1::"tvar prm"
   and   \<theta>::"Subst"
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/Nominal.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1262,19 +1262,21 @@
   apply (simp add: pt_rev_pi [OF pt at])
   done
 
-lemma insert_eqvt:
+lemma pt_insert_eqvt:
+  fixes pi::"'x prm"
+  and   x::"'a"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
-  shows "(pi::'x prm)\<bullet>(insert (x::'a) X) = insert (pi\<bullet>x) (pi\<bullet>X)"
+  shows "(pi\<bullet>(insert x X)) = insert (pi\<bullet>x) (pi\<bullet>X)"
   by (auto simp add: perm_set_eq [OF pt at])
 
-lemma set_eqvt:
+lemma pt_set_eqvt:
   fixes pi :: "'x prm"
   and   xs :: "'a list"
   assumes pt: "pt TYPE('a) TYPE('x)"
   and at: "at TYPE('x)" 
   shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)"
-by (induct xs) (auto simp add: empty_eqvt insert_eqvt [OF pt at])
+by (induct xs) (auto simp add: empty_eqvt pt_insert_eqvt [OF pt at])
 
 lemma supp_singleton:
   assumes pt: "pt TYPE('a) TYPE('x)"
@@ -1568,10 +1570,10 @@
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="pi\<bullet>xa" in bspec)
 apply(simp add: pt_set_bij1[OF ptb, OF at])
-apply(simp add: set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
+apply(simp add: pt_set_eqvt [OF ptb at] pt_rev_pi[OF pt_list_inst[OF ptb], OF at])
 apply(simp add: pt_fresh_bij_ineq[OF pta, OF ptb, OF at, OF cp])
 apply(drule_tac x="(rev pi)\<bullet>xa" in bspec)
-apply(simp add: pt_set_bij1[OF ptb, OF at] set_eqvt [OF ptb at])
+apply(simp add: pt_set_bij1[OF ptb, OF at] pt_set_eqvt [OF ptb at])
 apply(simp add: pt_fresh_left_ineq[OF pta, OF ptb, OF at, OF cp])
 done
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/nominal_atoms.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -798,8 +798,8 @@
        val pt_perm_supp_ineq   = @{thm "Nominal.pt_perm_supp_ineq"};
        val pt_perm_supp        = @{thm "Nominal.pt_perm_supp"};
        val subseteq_eqvt       = @{thm "Nominal.pt_subseteq_eqvt"};
-       val insert_eqvt         = @{thm "Nominal.insert_eqvt"};
-       val set_eqvt            = @{thm "Nominal.set_eqvt"};
+       val insert_eqvt         = @{thm "Nominal.pt_insert_eqvt"};
+       val set_eqvt            = @{thm "Nominal.pt_set_eqvt"};
        val perm_set_eq         = @{thm "Nominal.perm_set_eq"};
 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Nominal/nominal_primrec.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Nominal/nominal_primrec.ML
-    ID:         $Id$
     Author:     Stefan Berghofer, TU Muenchen and Norbert Voelker, FernUni Hagen
 
 Package for defining functions on nominal datatypes by primitive recursion.
@@ -8,14 +7,10 @@
 
 signature NOMINAL_PRIMREC =
 sig
-  val add_primrec: string -> string list option -> string option ->
-    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
-  val add_primrec_unchecked: string -> string list option -> string option ->
-    ((Binding.T * string) * Attrib.src list) list -> theory -> Proof.state
-  val add_primrec_i: string -> term list option -> term option ->
-    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
-  val add_primrec_unchecked_i: string -> term list option -> term option ->
-    ((Binding.T * term) * attribute list) list -> theory -> Proof.state
+  val add_primrec: term list option -> term option ->
+    (Binding.T * typ option * mixfix) list ->
+    (Binding.T * typ option * mixfix) list ->
+    (Attrib.binding * term) list -> local_theory -> Proof.state
 end;
 
 structure NominalPrimrec : NOMINAL_PRIMREC =
@@ -26,23 +21,31 @@
 exception RecError of string;
 
 fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
-fun primrec_eq_err thy s eq =
-  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term_global thy eq));
+fun primrec_eq_err lthy s eq =
+  primrec_err (s ^ "\nin\n" ^ quote (Syntax.string_of_term lthy eq));
 
 
 (* preprocessing of equations *)
 
-fun process_eqn thy eq rec_fns = 
+fun unquantify t =
   let
+    val (vs, Ts) = split_list (strip_qnt_vars "all" t);
+    val body = strip_qnt_body "all" t;
+    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+      (fn Free (v, _) => insert (op =) v | _ => I) body []))
+  in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;
+
+fun process_eqn lthy is_fixed spec rec_fns = 
+  let
+    val eq = unquantify spec;
     val (lhs, rhs) = 
-      if null (term_vars eq) then
-        HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
-        handle TERM _ => raise RecError "not a proper equation"
-      else raise RecError "illegal schematic variable(s)";
+      HOLogic.dest_eq (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))
+      handle TERM _ => raise RecError "not a proper equation";
 
     val (recfun, args) = strip_comb lhs;
-    val fnameT = dest_Const recfun handle TERM _ => 
-      raise RecError "function is not declared as constant in theory";
+    val fname = case recfun of Free (v, _) => if is_fixed v then v
+          else raise RecError "illegal head of function equation"
+      | _ => raise RecError "illegal head of function equation";
 
     val (ls', rest)  = take_prefix is_Free args;
     val (middle, rs') = take_suffix is_Free rest;
@@ -68,26 +71,28 @@
     else
      (check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
       check_vars "extra variables on rhs: "
-        (map dest_Free (term_frees rhs) \\ lfrees);
-      case AList.lookup (op =) rec_fns fnameT of
+        (map dest_Free (term_frees rhs) |> subtract (op =) lfrees
+          |> filter_out (is_fixed o fst));
+      case AList.lookup (op =) rec_fns fname of
         NONE =>
-          (fnameT, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
+          (fname, (tname, rpos, [(cname, (ls, cargs, rs, rhs, eq))]))::rec_fns
       | SOME (_, rpos', eqns) =>
           if AList.defined (op =) eqns cname then
             raise RecError "constructor already occurred as pattern"
           else if rpos <> rpos' then
             raise RecError "position of recursive argument inconsistent"
           else
-            AList.update (op =) (fnameT, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
+            AList.update (op =)
+              (fname, (tname, rpos, (cname, (ls, cargs, rs, rhs, eq))::eqns))
               rec_fns)
   end
-  handle RecError s => primrec_eq_err thy s eq;
+  handle RecError s => primrec_eq_err lthy s spec;
 
 val param_err = "Parameters must be the same for all recursive functions";
 
-fun process_fun thy descr rec_eqns (i, fnameT as (fname, _)) (fnameTs, fnss) =
+fun process_fun lthy descr eqns (i, fname) (fnames, fnss) =
   let
-    val (_, (tname, _, constrs)) = List.nth (descr, i);
+    val (_, (tname, _, constrs)) = nth descr i;
 
     (* substitute "fname ls x rs" by "y" for (x, (_, y)) in subs *)
 
@@ -100,16 +105,17 @@
           let
             val (f, ts) = strip_comb t;
           in
-            if is_Const f andalso dest_Const f mem map fst rec_eqns then
+            if is_Free f
+              andalso member (fn ((v, _), (w, _)) => v = w) eqns (dest_Free f) then
               let
-                val fnameT' as (fname', _) = dest_Const f;
-                val (_, rpos, eqns) = the (AList.lookup (op =) rec_eqns fnameT');
-                val ls = Library.take (rpos, ts);
-                val rest = Library.drop (rpos, ts);
-                val (x', rs) = (hd rest, tl rest)
-                  handle Empty => raise RecError ("not enough arguments\
-                   \ in recursive application\nof function " ^ quote fname' ^ " on rhs");
-                val rs' = (case eqns of
+                val (fname', _) = dest_Free f;
+                val (_, rpos, eqns') = the (AList.lookup (op =) eqns fname');
+                val (ls, rs'') = chop rpos ts
+                val (x', rs) = case rs'' of
+                    x' :: rs => (x', rs)
+                  | [] => raise RecError ("not enough arguments in recursive application\n"
+                      ^ "of function " ^ quote fname' ^ " on rhs");
+                val rs' = (case eqns' of
                     (_, (ls', _, rs', _, _)) :: _ =>
                       let val (rs1, rs2) = chop (length rs') rs
                       in
@@ -126,7 +132,7 @@
                 | SOME (i', y) =>
                     fs
                     |> fold_map (subst subs) (xs @ rs')
-                    ||> process_fun thy descr rec_eqns (i', fnameT')
+                    ||> process_fun lthy descr eqns (i', fname')
                     |-> (fn ts' => pair (list_comb (y, ts')))
               end
             else
@@ -138,41 +144,39 @@
 
     (* translate rec equations into function arguments suitable for rec comb *)
 
-    fun trans eqns (cname, cargs) (fnameTs', fnss', fns) =
+    fun trans eqns (cname, cargs) (fnames', fnss', fns) =
       (case AList.lookup (op =) eqns cname of
           NONE => (warning ("No equation for constructor " ^ quote cname ^
             "\nin definition of function " ^ quote fname);
-              (fnameTs', fnss', (Const (@{const_name undefined}, dummyT))::fns))
+              (fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns))
         | SOME (ls, cargs', rs, rhs, eq) =>
             let
               val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
               val rargs = map fst recs;
-              val subs = map (rpair dummyT o fst) 
+              val subs = map (rpair dummyT o fst)
                 (rev (rename_wrt_term rhs rargs));
-              val (rhs', (fnameTs'', fnss'')) = 
-                  (subst (map (fn ((x, y), z) =>
-                               (Free x, (body_index y, Free z)))
-                          (recs ~~ subs)) rhs (fnameTs', fnss'))
-                  handle RecError s => primrec_eq_err thy s eq
-            in (fnameTs'', fnss'', 
+              val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
+                (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
+                  handle RecError s => primrec_eq_err lthy s eq
+            in (fnames'', fnss'', 
                 (list_abs_free (cargs' @ subs, rhs'))::fns)
             end)
 
-  in (case AList.lookup (op =) fnameTs i of
+  in (case AList.lookup (op =) fnames i of
       NONE =>
-        if exists (equal fnameT o snd) fnameTs then
+        if exists (fn (_, v) => fname = v) fnames then
           raise RecError ("inconsistent functions for datatype " ^ quote tname)
         else
           let
-            val SOME (_, _, eqns as (_, (ls, _, rs, _, _)) :: _) =
-              AList.lookup (op =) rec_eqns fnameT;
-            val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
-              ((i, fnameT)::fnameTs, fnss, []) 
+            val SOME (_, _, eqns' as (_, (ls, _, rs, _, _)) :: _) =
+              AList.lookup (op =) eqns fname;
+            val (fnames', fnss', fns) = fold_rev (trans eqns') constrs
+              ((i, fname)::fnames, fnss, []) 
           in
-            (fnameTs', (i, (fname, ls, rs, fns))::fnss')
+            (fnames', (i, (fname, ls, rs, fns))::fnss')
           end
-    | SOME fnameT' =>
-        if fnameT = fnameT' then (fnameTs, fnss)
+    | SOME fname' =>
+        if fname = fname' then (fnames, fnss)
         else raise RecError ("inconsistent functions for datatype " ^ quote tname))
   end;
 
@@ -195,18 +199,21 @@
 
 (* make definition *)
 
-fun make_def thy fs (fname, ls, rs, rec_name, tname) =
+fun make_def ctxt fixes fs (fname, ls, rs, rec_name, tname) =
   let
     val used = map fst (fold Term.add_frees fs []);
     val x = (Name.variant used "x", dummyT);
     val frees = ls @ x :: rs;
-    val rhs = list_abs_free (frees,
+    val raw_rhs = list_abs_free (frees,
       list_comb (Const (rec_name, dummyT), fs @ [Free x]))
-    val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
-    val def_prop as _ $ _ $ t =
-      singleton (Syntax.check_terms (ProofContext.init thy))
-        (Logic.mk_equals (Const (fname, dummyT), rhs));
-  in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
+    val def_name = Thm.def_name (Sign.base_name fname);
+    val rhs = singleton (Syntax.check_terms ctxt) raw_rhs;
+    val SOME var = get_first (fn ((b, _), mx) =>
+      if Binding.base_name b = fname then SOME (b, mx) else NONE) fixes;
+  in
+    ((var, ((Binding.name def_name, []), rhs)),
+     subst_bounds (rev (map Free frees), strip_abs_body rhs))
+  end;
 
 
 (* find datatypes which contain all datatypes in tnames' *)
@@ -227,27 +234,36 @@
 
 local
 
-fun gen_primrec_i note def alt_name invs fctxt eqns_atts thy =
+fun prepare_spec prep_spec ctxt raw_fixes raw_spec =
+  let
+    val ((fixes, spec), _) = prep_spec
+      raw_fixes (map (single o apsnd single) raw_spec) ctxt
+  in (fixes, map (apsnd the_single) spec) end;
+
+fun gen_primrec set_group prep_spec prep_term invs fctxt raw_fixes raw_params raw_spec lthy =
   let
-    val (raw_eqns, atts) = split_list eqns_atts;
-    val eqns = map (apfst Binding.base_name) raw_eqns;
-    val dt_info = NominalPackage.get_nominal_datatypes thy;
-    val rec_eqns = fold_rev (process_eqn thy o snd) eqns [];
+    val (fixes', spec) = prepare_spec prep_spec lthy (raw_fixes @ raw_params) raw_spec;
+    val fixes = List.take (fixes', length raw_fixes);
+    val (names_atts, spec') = split_list spec;
+    val eqns' = map unquantify spec'
+    val eqns = fold_rev (process_eqn lthy (fn v => Variable.is_fixed lthy v
+      orelse exists (fn ((w, _), _) => v = Binding.base_name w) fixes)) spec' [];
+    val dt_info = NominalPackage.get_nominal_datatypes (ProofContext.theory_of lthy);
     val lsrs :: lsrss = maps (fn (_, (_, _, eqns)) =>
-      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) rec_eqns
+      map (fn (_, (ls, _, rs, _, _)) => ls @ rs) eqns) eqns
     val _ =
       (if forall (curry eq_set lsrs) lsrss andalso forall
          (fn (_, (_, _, (_, (ls, _, rs, _, _)) :: eqns)) =>
                forall (fn (_, (ls', _, rs', _, _)) =>
                  ls = ls' andalso rs = rs') eqns
-           | _ => true) rec_eqns
+           | _ => true) eqns
        then () else primrec_err param_err);
-    val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
+    val tnames = distinct (op =) (map (#1 o snd) eqns);
     val dts = find_dts dt_info tnames tnames;
     val main_fns = 
       map (fn (tname, {index, ...}) =>
         (index, 
-          (fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
+          (fst o the o find_first (fn (_, x) => #1 x = tname)) eqns))
       dts;
     val {descr, rec_names, rec_rewrites, ...} = 
       if null dts then
@@ -256,32 +272,32 @@
     val descr = map (fn (i, (tname, args, constrs)) => (i, (tname, args,
       map (fn (cname, cargs) => (cname, fold (fn (dTs, dT) => fn dTs' =>
         dTs' @ dTs @ [dT]) cargs [])) constrs))) descr;
-    val (fnameTs, fnss) =
-      fold_rev (process_fun thy descr rec_eqns) main_fns ([], []);
+    val (fnames, fnss) = fold_rev (process_fun lthy descr eqns) main_fns ([], []);
     val (fs, defs) = fold_rev (get_fns fnss) (descr ~~ rec_names) ([], []);
-    val defs' = map (make_def thy fs) defs;
-    val nameTs1 = map snd fnameTs;
-    val nameTs2 = map fst rec_eqns;
-    val _ = if gen_eq_set (op =) (nameTs1, nameTs2) then ()
-            else primrec_err ("functions " ^ commas_quote (map fst nameTs2) ^
-              "\nare not mutually recursive");
-    val primrec_name =
-      if alt_name = "" then (space_implode "_" (map (Sign.base_name o #1) defs)) else alt_name;
-    val (defs_thms', thy') =
-      thy
-      |> Sign.add_path primrec_name
-      |> fold_map def (map (fn ((name, t), _) => ((name, []), t)) defs');
-    val cert = cterm_of thy';
+    val defs' = map (make_def lthy fixes fs) defs;
+    val names1 = map snd fnames;
+    val names2 = map fst eqns;
+    val _ = if gen_eq_set (op =) (names1, names2) then ()
+      else primrec_err ("functions " ^ commas_quote names2 ^
+        "\nare not mutually recursive");
+    val (defs_thms, lthy') = lthy |>
+      set_group ? LocalTheory.set_group (serial_string ()) |>
+      fold_map (apfst (snd o snd) oo
+        LocalTheory.define Thm.definitionK o fst) defs';
+    val qualify = Binding.qualify
+      (space_implode "_" (map (Sign.base_name o #1) defs));
+    val names_atts' = map (apfst qualify) names_atts;
+    val cert = cterm_of (ProofContext.theory_of lthy');
 
     fun mk_idx eq =
       let
-        val Const c = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
+        val Free (name, _) = head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop
           (Logic.strip_imp_concl eq))));
-        val SOME i = AList.lookup op = (map swap fnameTs) c;
+        val SOME i = AList.lookup op = (map swap fnames) name;
         val SOME (_, _, constrs) = AList.lookup op = descr i;
-        val SOME (_, _, eqns) = AList.lookup op = rec_eqns c;
+        val SOME (_, _, eqns'') = AList.lookup op = eqns name;
         val SOME (cname, (_, cargs, _, _, _)) = find_first
-          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns
+          (fn (_, (_, _, _, _, eq')) => eq = eq') eqns''
       in (i, find_index (fn (cname', _) => cname = cname') constrs, cargs) end;
 
     val rec_rewritess =
@@ -296,19 +312,15 @@
       curry (List.take o swap) (length fvars) |> map cert;
     val invs' = (case invs of
         NONE => map (fn (i, _) =>
-          let
-            val SOME (_, T) = AList.lookup op = fnameTs i
-            val (Ts, U) = strip_type T
-          in
-            Abs ("x", List.drop (Ts, length lsrs + 1) ---> U, HOLogic.true_const)
-          end) descr
-      | SOME invs' => invs');
+          Abs ("x", fastype_of (snd (nth defs' i)), HOLogic.true_const)) descr
+      | SOME invs' => map (prep_term lthy') invs');
     val inst = (map cert fvars ~~ cfs) @
       (map (cert o Var) pvars ~~ map cert invs') @
       (case ctxtvars of
-         [ctxtvar] => [(cert (Var ctxtvar), cert (the_default HOLogic.unit fctxt))]
+         [ctxtvar] => [(cert (Var ctxtvar),
+           cert (the_default HOLogic.unit (Option.map (prep_term lthy') fctxt)))]
        | _ => []);
-    val rec_rewrites' = map (fn (_, eq) =>
+    val rec_rewrites' = map (fn eq =>
       let
         val (i, j, cargs) = mk_idx eq
         val th = nth (nth rec_rewritess i) j;
@@ -317,8 +329,8 @@
           strip_comb |> snd
       in (cargs, Logic.strip_imp_prems eq,
         Drule.cterm_instantiate (inst @
-          (map (cterm_of thy') cargs' ~~ map (cterm_of thy' o Free) cargs)) th)
-      end) eqns;
+          (map cert cargs' ~~ map (cert o Free) cargs)) th)
+      end) eqns';
 
     val prems = foldr1 (common_prefix op aconv) (map (prems_of o #3) rec_rewrites');
     val cprems = map cert prems;
@@ -346,64 +358,37 @@
     val rule = implies_intr_list rule_prems
       (Conjunction.intr_balanced (map mk_eqn (rec_rewrites' ~~ asmss)));
 
-    val goals = map (fn ((cargs, _, _), (_, eqn)) =>
-      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns);
+    val goals = map (fn ((cargs, _, _), eqn) =>
+      (list_all_free (cargs, eqn), [])) (rec_rewrites' ~~ eqns');
 
   in
-    thy' |>
-    ProofContext.init |>
+    lthy' |>
+    Variable.add_fixes (map fst lsrs) |> snd |>
     Proof.theorem_i NONE
-      (fn thss => ProofContext.theory (fn thy =>
+      (fn thss => fn goal_ctxt =>
          let
-           val simps = map standard (flat thss);
-           val (simps', thy') =
-             fold_map note ((map fst eqns ~~ atts) ~~ map single simps) thy;
-           val simps'' = maps snd simps'
+           val simps = ProofContext.export goal_ctxt lthy' (flat thss);
+           val (simps', lthy'') = fold_map (LocalTheory.note Thm.theoremK)
+             (names_atts' ~~ map single simps) lthy'
          in
-           thy'
-           |> note (("simps", [Simplifier.simp_add]), simps'')
+           lthy''
+           |> LocalTheory.note Thm.theoremK ((qualify (Binding.name "simps"),
+             [Attrib.internal (K Simplifier.simp_add)]), maps snd simps')
            |> snd
-           |> Sign.parent_path
-         end))
+         end)
       [goals] |>
     Proof.apply (Method.Basic (fn _ => Method.RAW_METHOD (fn _ =>
-      rewrite_goals_tac (map snd defs_thms') THEN
+      rewrite_goals_tac defs_thms THEN
       compose_tac (false, rule, length rule_prems) 1), Position.none)) |>
     Seq.hd
   end;
 
-fun gen_primrec note def alt_name invs fctxt eqns thy =
-  let
-    val ((names, strings), srcss) = apfst split_list (split_list eqns);
-    val atts = map (map (Attrib.attribute thy)) srcss;
-    val eqn_ts = map (fn s => Syntax.read_prop_global thy s
-      handle ERROR msg => cat_error msg ("The error(s) above occurred for " ^ s)) strings;
-    val rec_ts = map (fn eq => head_of (fst (HOLogic.dest_eq
-      (HOLogic.dest_Trueprop (Logic.strip_imp_concl eq))))
-      handle TERM _ => primrec_eq_err thy "not a proper equation" eq) eqn_ts;
-    val (_, eqn_ts') = OldPrimrecPackage.unify_consts thy rec_ts eqn_ts
-  in
-    gen_primrec_i note def alt_name
-      (Option.map (map (Syntax.read_term_global thy)) invs)
-      (Option.map (Syntax.read_term_global thy) fctxt)
-      (names ~~ eqn_ts' ~~ atts) thy
-  end;
-
-fun thy_note ((name, atts), thms) =
-  PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms));
-fun thy_def false ((name, atts), t) =
-      PureThy.add_defs false [((name, t), atts)] #-> (fn [thm] => pair (name, thm))
-  | thy_def true ((name, atts), t) =
-      PureThy.add_defs_unchecked false [((name, t), atts)] #-> (fn [thm] => pair (name, thm));
-
 in
 
-val add_primrec = gen_primrec thy_note (thy_def false);
-val add_primrec_unchecked = gen_primrec thy_note (thy_def true);
-val add_primrec_i = gen_primrec_i thy_note (thy_def false);
-val add_primrec_unchecked_i = gen_primrec_i thy_note (thy_def true);
+val add_primrec = gen_primrec false Specification.check_specification (K I);
+val add_primrec_cmd = gen_primrec true Specification.read_specification Syntax.read_term;
 
-end; (*local*)
+end;
 
 
 (* outer syntax *)
@@ -419,25 +404,26 @@
 val parser2 = (invariant -- P.$$$ ":") |--
     (Scan.repeat1 (unless_flag P.term) >> SOME) -- Scan.optional parser1 NONE ||
   (parser1 >> pair NONE);
-val parser3 =
-  unless_flag P.name -- Scan.optional parser2 (NONE, NONE) ||
-  (parser2 >> pair "");
-val parser4 =
-  (P.$$$ "unchecked" >> K true) -- Scan.optional parser3 ("", (NONE, NONE)) ||
-  (parser3 >> pair false);
 val options =
   Scan.optional (P.$$$ "(" |-- P.!!!
-    (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE)));
+    (parser2 --| P.$$$ ")")) (NONE, NONE);
+
+fun pipe_error t = P.!!! (Scan.fail_with (K
+  (cat_lines ["Equations must be separated by " ^ quote "|", quote t])));
 
-val primrec_decl =
-  options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop);
+val statement = SpecParse.opt_thm_name ":" -- P.prop --| Scan.ahead
+  ((P.term :-- pipe_error) || Scan.succeed ("",""));
+
+val statements = P.enum1 "|" statement;
+
+val primrec_decl = P.opt_target -- options --
+  P.fixes -- P.for_fixes --| P.$$$ "where" -- statements;
 
 val _ =
   OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal
-    (primrec_decl >> (fn ((unchecked, (alt_name, (invs, fctxt))), eqns) =>
-      Toplevel.print o Toplevel.theory_to_proof
-        ((if unchecked then add_primrec_unchecked else add_primrec) alt_name invs fctxt
-          (map P.triple_swap eqns))));
+    (primrec_decl >> (fn ((((opt_target, (invs, fctxt)), raw_fixes), raw_params), raw_spec) =>
+      Toplevel.print o Toplevel.local_theory_to_proof opt_target
+        (add_primrec_cmd invs fctxt raw_fixes raw_params raw_spec)));
 
 end;
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Real.thy
--- a/src/HOL/Real.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Real.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,5 @@
 theory Real
-imports "~~/src/HOL/Real/RealVector"
+imports RComplete "~~/src/HOL/Real/RealVector"
 begin
 
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/atp_manager.ML
--- a/src/HOL/Tools/atp_manager.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Tools/atp_manager.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/atp_manager.ML
-    ID:         $Id$
     Author:     Fabian Immler, TU Muenchen
 
 ATP threads are registered here.
@@ -19,6 +18,7 @@
   val set_timeout: int -> unit
   val kill: unit -> unit
   val info: unit -> unit
+  val messages: int option -> unit
   type prover = int -> Proof.state -> bool * string
   val add_prover: string -> prover -> theory -> theory
   val print_provers: theory -> unit
@@ -30,6 +30,9 @@
 
 (** preferences **)
 
+val message_store_limit = 20;
+val message_display_limit = 5;
+
 local
 
 val atps = ref "e";
@@ -85,13 +88,14 @@
  {timeout_heap: ThreadHeap.T,
   oldest_heap: ThreadHeap.T,
   active: (Thread.thread * (Time.time * Time.time * string)) list,
-  cancelling: (Thread.thread * (Time.time * Time.time * string)) list};
+  cancelling: (Thread.thread * (Time.time * Time.time * string)) list,
+  messages: string list};
 
-fun make_state timeout_heap oldest_heap active cancelling =
+fun make_state timeout_heap oldest_heap active cancelling messages =
   State {timeout_heap = timeout_heap, oldest_heap = oldest_heap,
-    active = active, cancelling = cancelling};
+    active = active, cancelling = cancelling, messages = messages};
 
-val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] []);
+val state = Synchronized.var "atp_manager" (make_state ThreadHeap.empty ThreadHeap.empty [] [] []);
 
 
 (* the managing thread *)
@@ -103,7 +107,7 @@
 (* unregister thread from thread manager -- move to cancelling *)
 
 fun unregister (success, message) thread = Synchronized.change_result state
-  (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
     let
       val info = lookup_thread active thread
 
@@ -127,7 +131,12 @@
         | SOME (_, _, desc) => "Sledgehammer: " ^ desc ^ "\n" ^ message ^
           (if null group_threads then ""
            else "\nInterrupted " ^ string_of_int (length group_threads - 1) ^ " other group members")
-    in (message', make_state timeout_heap oldest_heap active'' cancelling'') end);
+
+      val messages' = case info of NONE => messages
+        | SOME (_, _, desc) => desc ^ "\n" ^ message ::
+           (if length messages <= message_store_limit then messages
+            else #1 (chop message_store_limit messages))
+    in (message', make_state timeout_heap oldest_heap active'' cancelling'' messages') end);
 
 
 (* kill excessive atp threads *)
@@ -140,12 +149,13 @@
 
 fun kill_oldest () =
   let exception Unchanged in
-    Synchronized.change_result state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+    Synchronized.change_result state
+      (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
         if ThreadHeap.is_empty oldest_heap orelse not (excessive_atps active)
         then raise Unchanged
         else
           let val ((_, oldest_thread), oldest_heap') = ThreadHeap.min_elem oldest_heap
-          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling) end)
+          in (oldest_thread, make_state timeout_heap oldest_heap' active cancelling messages) end)
       |> (priority o unregister (false, "Interrupted (maximum number of ATPs exceeded)"))
     handle Unchanged => ()
   end;
@@ -175,7 +185,7 @@
         | SOME (time, _) => SOME time)
 
       (* action: cancel find threads whose timeout is reached, and interrupt cancelling threads *)
-      fun action (State {timeout_heap, oldest_heap, active, cancelling}) =
+      fun action (State {timeout_heap, oldest_heap, active, cancelling, messages}) =
         let val (timeout_threads, timeout_heap') =
           ThreadHeap.upto (Time.now (), Thread.self ()) timeout_heap
         in
@@ -185,7 +195,7 @@
             let
               val _ = List.app (SimpleThread.interrupt o #1) cancelling
               val cancelling' = filter (Thread.isActive o #1) cancelling
-              val state' = make_state timeout_heap' oldest_heap active cancelling'
+              val state' = make_state timeout_heap' oldest_heap active cancelling' messages
             in SOME (map #2 timeout_threads, state') end
         end
     in
@@ -203,12 +213,13 @@
 
 fun register birthtime deadtime (thread, desc) =
  (check_thread_manager ();
-  Synchronized.change state (fn State {timeout_heap, oldest_heap, active, cancelling} =>
-    let
-      val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
-      val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
-      val active' = update_thread (thread, (birthtime, deadtime, desc)) active
-    in make_state timeout_heap' oldest_heap' active' cancelling end));
+  Synchronized.change state
+    (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
+      let
+        val timeout_heap' = ThreadHeap.insert (deadtime, thread) timeout_heap
+        val oldest_heap' = ThreadHeap.insert (birthtime, thread) oldest_heap
+        val active' = update_thread (thread, (birthtime, deadtime, desc)) active
+      in make_state timeout_heap' oldest_heap' active' cancelling messages end));
 
 
 
@@ -217,16 +228,17 @@
 (* kill: move all threads to cancelling *)
 
 fun kill () = Synchronized.change state
-  (fn State {timeout_heap, oldest_heap, active, cancelling} =>
+  (fn State {timeout_heap, oldest_heap, active, cancelling, messages} =>
     let val formerly_active = map (fn (th, (tb, _, desc)) => (th, (tb, Time.now (), desc))) active
-    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) end);
+    in make_state timeout_heap oldest_heap [] (formerly_active @ cancelling) messages end);
 
 
-(* info: information on running threads *)
+(* ATP info *)
 
 fun info () =
   let
-    val State {timeout_heap, oldest_heap, active, cancelling} = Synchronized.value state
+    val State {active, cancelling, ...} = Synchronized.value state
+
     fun running_info (_, (birth_time, dead_time, desc)) = "Running: "
         ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), birth_time))
         ^ " s  --  "
@@ -235,6 +247,7 @@
     fun cancelling_info (_, (_, dead_time, desc)) = "Trying to interrupt thread since "
         ^ (string_of_int o Time.toSeconds) (Time.- (Time.now (), dead_time))
         ^ " s:\n" ^ desc
+
     val running =
       if null active then "No ATPs running."
       else space_implode "\n\n" ("Running ATPs:" :: map running_info active)
@@ -242,8 +255,17 @@
       if null cancelling then ""
       else space_implode "\n\n"
         ("Trying to interrupt the following ATPs:" :: map cancelling_info cancelling)
+
   in writeln (running ^ "\n" ^ interrupting) end;
 
+fun messages opt_limit =
+  let
+    val limit = the_default message_display_limit opt_limit;
+    val State {messages = msgs, ...} = Synchronized.value state
+    val header = "Recent ATP messages" ^
+      (if length msgs <= limit then ":" else " (" ^ string_of_int limit ^ " displayed):");
+  in writeln (space_implode "\n\n" (header :: #1 (chop limit msgs))) end;
+
 
 
 (** The Sledgehammer **)
@@ -322,6 +344,11 @@
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
 
 val _ =
+  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
+    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+
+val _ =
   OuterSyntax.improper_command "print_atps" "print external provers" K.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
       Toplevel.keep (print_provers o Toplevel.theory_of)));
@@ -329,7 +356,7 @@
 val _ =
   OuterSyntax.command "sledgehammer" "call all automatic theorem provers" K.diag
     (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
-    Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
+      Toplevel.keep ((sledgehammer names) o Toplevel.proof_of)));
 
 end;
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/decompose.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/decompose.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,105 @@
+(*  Title:       HOL/Tools/function_package/decompose.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Graph decomposition using "Shallow Dependency Pairs".
+*)
+
+signature DECOMPOSE =
+sig
+
+  val derive_chains : Proof.context -> tactic
+                      -> (Termination.data -> int -> tactic)
+                      -> Termination.data -> int -> tactic
+
+  val decompose_tac : Proof.context -> tactic
+                      -> Termination.ttac
+
+end
+
+structure Decompose : DECOMPOSE =
+struct
+
+structure TermGraph = GraphFun(type key = term val ord = Term.fast_term_ord);
+
+
+fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
+  let
+      val thy = ProofContext.theory_of ctxt
+
+      fun prove_chain c1 c2 D =
+          if is_some (Termination.get_chain D c1 c2) then D else
+          let
+            val goal = HOLogic.mk_eq (HOLogic.mk_binop @{const_name "Relation.rel_comp"} (c1, c2),
+                                      Const (@{const_name "{}"}, fastype_of c1))
+                       |> HOLogic.mk_Trueprop (* "C1 O C2 = {}" *)
+
+            val chain = case FundefLib.try_proof (cterm_of thy goal) chain_tac of
+                          FundefLib.Solved thm => SOME thm
+                        | _ => NONE
+          in
+            Termination.note_chain c1 c2 chain D
+          end
+  in
+    cont (fold_product prove_chain cs cs D) i
+  end)
+
+
+fun mk_dgraph D cs =
+    TermGraph.empty
+    |> fold (fn c => TermGraph.new_node (c,())) cs
+    |> fold_product (fn c1 => fn c2 =>
+         if is_none (Termination.get_chain D c1 c2 |> the_default NONE)
+         then TermGraph.add_edge (c1, c2) else I)
+       cs cs
+
+
+fun ucomp_empty_tac T =
+    REPEAT_ALL_NEW (rtac @{thm union_comp_emptyR}
+                    ORELSE' rtac @{thm union_comp_emptyL}
+                    ORELSE' SUBGOAL (fn (_ $ (_ $ (_ $ c1 $ c2) $ _), i) => rtac (T c1 c2) i))
+
+fun regroup_calls_tac cs = Termination.CALLS (fn (cs', i) =>
+   let
+     val is = map (fn c => find_index (curry op aconv c) cs') cs
+   in
+     CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv is))) i
+   end)
+
+
+fun solve_trivial_tac D = Termination.CALLS
+(fn ([c], i) =>
+    (case Termination.get_chain D c c of
+       SOME (SOME thm) => rtac @{thm wf_no_loop} i
+                          THEN rtac thm i
+     | _ => no_tac)
+  | _ => no_tac)
+
+fun decompose_tac' ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+    let
+      val G = mk_dgraph D cs
+      val sccs = TermGraph.strong_conn G
+
+      fun split [SCC] i = (solve_trivial_tac D i ORELSE cont D i)
+        | split (SCC::rest) i =
+            regroup_calls_tac SCC i
+            THEN rtac @{thm wf_union_compatible} i
+            THEN rtac @{thm less_by_empty} (i + 2)
+            THEN ucomp_empty_tac (the o the oo Termination.get_chain D) (i + 2)
+            THEN split rest (i + 1)
+            THEN (solve_trivial_tac D i ORELSE cont D i)
+    in
+      if length sccs > 1 then split sccs i
+      else solve_trivial_tac D i ORELSE err_cont D i
+    end)
+
+fun decompose_tac ctxt chain_tac cont err_cont =
+    derive_chains ctxt chain_tac
+    (decompose_tac' ctxt cont err_cont)
+
+fun auto_decompose_tac ctxt =
+    Termination.TERMINATION ctxt
+      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
+                     (K (K all_tac)) (K (K no_tac)))
+
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/descent.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/descent.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,44 @@
+(*  Title:       HOL/Tools/function_package/descent.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Descent proofs for termination
+*)
+
+
+signature DESCENT =
+sig
+
+  val derive_diag : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+  val derive_all  : Proof.context -> tactic -> (Termination.data -> int -> tactic)
+                    -> Termination.data -> int -> tactic
+
+end
+
+
+structure Descent : DESCENT =
+struct
+
+fun gen_descent diag ctxt tac cont D = Termination.CALLS (fn (cs, i) =>
+  let
+    val thy = ProofContext.theory_of ctxt
+    val measures_of = Termination.get_measures D
+
+    fun derive c D =
+      let
+        val (_, p, _, q, _, _) = Termination.dest_call D c
+      in
+        if diag andalso p = q
+        then fold (fn m => Termination.derive_descent thy tac c m m) (measures_of p) D
+        else fold_product (Termination.derive_descent thy tac c)
+               (measures_of p) (measures_of q) D
+      end
+  in
+    cont (FundefCommon.PROFILE "deriving descents" (fold derive cs) D) i
+  end)
+
+val derive_diag = gen_descent true
+val derive_all = gen_descent false
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/fundef_lib.ML
--- a/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_lib.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -130,4 +130,50 @@
     | SOME st => if Thm.no_prems st then Solved (Goal.finish st) else Stuck st
 
 
+fun dest_binop_list cn (t as (Const (n, _) $ a $ b)) = 
+    if cn = n then dest_binop_list cn a @ dest_binop_list cn b else [ t ]
+  | dest_binop_list _ t = [ t ]
+
+
+(* separate two parts in a +-expression:
+   "a + b + c + d + e" --> "(a + b + d) + (c + e)"
+
+   Here, + can be any binary operation that is AC.
+
+   cn - The name of the binop-constructor (e.g. @{const_name "op Un"})
+   ac - the AC rewrite rules for cn
+   is - the list of indices of the expressions that should become the first part
+        (e.g. [0,1,3] in the above example)
+*)
+
+fun regroup_conv neu cn ac is ct =
+ let
+   val mk = HOLogic.mk_binop cn
+   val t = term_of ct
+   val xs = dest_binop_list cn t
+   val js = 0 upto (length xs) - 1 \\ is
+   val ty = fastype_of t
+   val thy = theory_of_cterm ct
+ in
+   Goal.prove_internal []
+     (cterm_of thy
+       (Logic.mk_equals (t,
+          if is = []
+          then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
+          else if js = []
+            then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
+            else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
+     (K (MetaSimplifier.rewrite_goals_tac ac
+         THEN rtac Drule.reflexive_thm 1))
+ end
+
+(* instance for unions *)
+fun regroup_union_conv t =
+    regroup_conv (@{const_name "{}"})
+                  @{const_name "op Un"}
+       (map (fn t => t RS eq_reflection) (@{thms "Un_ac"} @
+                                          @{thms "Un_empty_right"} @
+                                          @{thms "Un_empty_left"})) t
+
+
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/scnp_reconstruct.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_reconstruct.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,426 @@
+(*  Title:       HOL/Tools/function_package/scnp_reconstruct.ML
+    Author:      Armin Heller, TU Muenchen
+    Author:      Alexander Krauss, TU Muenchen
+
+Proof reconstruction for SCNP
+*)
+
+signature SCNP_RECONSTRUCT =
+sig
+
+  val decomp_scnp : ScnpSolve.label list -> Proof.context -> method
+
+  val setup : theory -> theory
+
+  datatype multiset_setup =
+    Multiset of
+    {
+     msetT : typ -> typ,
+     mk_mset : typ -> term list -> term,
+     mset_regroup_conv : int list -> conv,
+     mset_member_tac : int -> int -> tactic,
+     mset_nonempty_tac : int -> tactic,
+     mset_pwleq_tac : int -> tactic,
+     set_of_simps : thm list,
+     smsI' : thm,
+     wmsI2'' : thm,
+     wmsI1 : thm,
+     reduction_pair : thm
+    }
+
+
+  val multiset_setup : multiset_setup -> theory -> theory
+
+end
+
+structure ScnpReconstruct : SCNP_RECONSTRUCT =
+struct
+
+val PROFILE = FundefCommon.PROFILE
+fun TRACE x = if ! FundefCommon.profile then Output.tracing x else ()
+
+open ScnpSolve
+
+val natT = HOLogic.natT
+val nat_pairT = HOLogic.mk_prodT (natT, natT)
+
+(* Theory dependencies *)
+
+datatype multiset_setup =
+  Multiset of
+  {
+   msetT : typ -> typ,
+   mk_mset : typ -> term list -> term,
+   mset_regroup_conv : int list -> conv,
+   mset_member_tac : int -> int -> tactic,
+   mset_nonempty_tac : int -> tactic,
+   mset_pwleq_tac : int -> tactic,
+   set_of_simps : thm list,
+   smsI' : thm,
+   wmsI2'' : thm,
+   wmsI1 : thm,
+   reduction_pair : thm
+  }
+
+structure MultisetSetup = TheoryDataFun
+(
+  type T = multiset_setup option
+  val empty = NONE
+  val copy = I;
+  val extend = I;
+  fun merge _ (v1, v2) = if is_some v2 then v2 else v1
+)
+
+val multiset_setup = MultisetSetup.put o SOME
+
+fun undef x = error "undef"
+fun get_multiset_setup thy = MultisetSetup.get thy
+  |> the_default (Multiset
+{ msetT = undef, mk_mset=undef,
+  mset_regroup_conv=undef, mset_member_tac = undef,
+  mset_nonempty_tac = undef, mset_pwleq_tac = undef,
+  set_of_simps = [],reduction_pair = refl,
+  smsI'=refl, wmsI2''=refl, wmsI1=refl })
+
+fun order_rpair _ MAX = @{thm max_rpair_set}
+  | order_rpair msrp MS  = msrp
+  | order_rpair _ MIN = @{thm min_rpair_set}
+
+fun ord_intros_max true =
+    (@{thm smax_emptyI}, @{thm smax_insertI})
+  | ord_intros_max false =
+    (@{thm wmax_emptyI}, @{thm wmax_insertI})
+fun ord_intros_min true =
+    (@{thm smin_emptyI}, @{thm smin_insertI})
+  | ord_intros_min false =
+    (@{thm wmin_emptyI}, @{thm wmin_insertI})
+
+fun gen_probl D cs =
+  let
+    val n = Termination.get_num_points D
+    val arity = length o Termination.get_measures D
+    fun measure p i = nth (Termination.get_measures D p) i
+
+    fun mk_graph c =
+      let
+        val (_, p, _, q, _, _) = Termination.dest_call D c
+
+        fun add_edge i j =
+          case Termination.get_descent D c (measure p i) (measure q j)
+           of SOME (Termination.Less _) => cons (i, GTR, j)
+            | SOME (Termination.LessEq _) => cons (i, GEQ, j)
+            | _ => I
+
+        val edges =
+          fold_product add_edge (0 upto arity p - 1) (0 upto arity q - 1) []
+      in
+        G (p, q, edges)
+      end
+  in
+    GP (map arity (0 upto n - 1), map mk_graph cs)
+  end
+
+(* General reduction pair application *)
+fun rem_inv_img ctxt =
+  let
+    val unfold_tac = LocalDefs.unfold_tac ctxt
+  in
+    rtac @{thm subsetI} 1
+    THEN etac @{thm CollectE} 1
+    THEN REPEAT (etac @{thm exE} 1)
+    THEN unfold_tac @{thms inv_image_def}
+    THEN rtac @{thm CollectI} 1
+    THEN etac @{thm conjE} 1
+    THEN etac @{thm ssubst} 1
+    THEN unfold_tac (@{thms split_conv} @ @{thms triv_forall_equality}
+                     @ @{thms Sum_Type.sum_cases})
+  end
+
+(* Sets *)
+
+val setT = HOLogic.mk_setT
+
+fun mk_set T [] = Const (@{const_name "{}"}, setT T)
+  | mk_set T (x :: xs) =
+      Const (@{const_name insert}, T --> setT T --> setT T) $
+            x $ mk_set T xs
+
+fun set_member_tac m i =
+  if m = 0 then rtac @{thm insertI1} i
+  else rtac @{thm insertI2} i THEN set_member_tac (m - 1) i
+
+val set_nonempty_tac = rtac @{thm insert_not_empty}
+
+fun set_finite_tac i =
+  rtac @{thm finite.emptyI} i
+  ORELSE (rtac @{thm finite.insertI} i THEN (fn st => set_finite_tac i st))
+
+
+(* Reconstruction *)
+
+fun reconstruct_tac ctxt D cs (gp as GP (_, gs)) certificate =
+  let
+    val thy = ProofContext.theory_of ctxt
+    val Multiset
+          { msetT, mk_mset,
+            mset_regroup_conv, mset_member_tac,
+            mset_nonempty_tac, mset_pwleq_tac, set_of_simps,
+            smsI', wmsI2'', wmsI1, reduction_pair=ms_rp } 
+        = get_multiset_setup thy
+
+    fun measure_fn p = nth (Termination.get_measures D p)
+
+    fun get_desc_thm cidx m1 m2 bStrict =
+      case Termination.get_descent D (nth cs cidx) m1 m2
+       of SOME (Termination.Less thm) =>
+          if bStrict then thm
+          else (thm COMP (Thm.lift_rule (cprop_of thm) @{thm less_imp_le}))
+        | SOME (Termination.LessEq (thm, _))  =>
+          if not bStrict then thm
+          else sys_error "get_desc_thm"
+        | _ => sys_error "get_desc_thm"
+
+    val (label, lev, sl, covering) = certificate
+
+    fun prove_lev strict g =
+      let
+        val G (p, q, el) = nth gs g
+
+        fun less_proof strict (j, b) (i, a) =
+          let
+            val tag_flag = b < a orelse (not strict andalso b <= a)
+
+            val stored_thm =
+              get_desc_thm g (measure_fn p i) (measure_fn q j)
+                             (not tag_flag)
+              |> Conv.fconv_rule (Thm.beta_conversion true)
+
+            val rule = if strict
+              then if b < a then @{thm pair_lessI2} else @{thm pair_lessI1}
+              else if b <= a then @{thm pair_leqI2} else @{thm pair_leqI1}
+          in
+            rtac rule 1 THEN PRIMITIVE (Thm.elim_implies stored_thm)
+            THEN (if tag_flag then arith_tac ctxt 1 else all_tac)
+          end
+
+        fun steps_tac MAX strict lq lp =
+          let
+            val (empty, step) = ord_intros_max strict
+          in
+            if length lq = 0
+            then rtac empty 1 THEN set_finite_tac 1
+                 THEN (if strict then set_nonempty_tac 1 else all_tac)
+            else
+              let
+                val (j, b) :: rest = lq
+                val (i, a) = the (covering g strict j)
+                fun choose xs = set_member_tac (Library.find_index (curry op = (i, a)) xs) 1
+                val solve_tac = choose lp THEN less_proof strict (j, b) (i, a)
+              in
+                rtac step 1 THEN solve_tac THEN steps_tac MAX strict rest lp
+              end
+          end
+          | steps_tac MIN strict lq lp =
+          let
+            val (empty, step) = ord_intros_min strict
+          in
+            if length lp = 0
+            then rtac empty 1
+                 THEN (if strict then set_nonempty_tac 1 else all_tac)
+            else
+              let
+                val (i, a) :: rest = lp
+                val (j, b) = the (covering g strict i)
+                fun choose xs = set_member_tac (Library.find_index (curry op = (j, b)) xs) 1
+                val solve_tac = choose lq THEN less_proof strict (j, b) (i, a)
+              in
+                rtac step 1 THEN solve_tac THEN steps_tac MIN strict lq rest
+              end
+          end
+          | steps_tac MS strict lq lp =
+          let
+            fun get_str_cover (j, b) =
+              if is_some (covering g true j) then SOME (j, b) else NONE
+            fun get_wk_cover (j, b) = the (covering g false j)
+
+            val qs = lq \\ map_filter get_str_cover lq
+            val ps = map get_wk_cover qs
+
+            fun indices xs ys = map (fn y => Library.find_index (curry op = y) xs) ys
+            val iqs = indices lq qs
+            val ips = indices lp ps
+
+            local open Conv in
+            fun t_conv a C =
+              params_conv ~1 (K ((concl_conv ~1 o arg_conv o arg1_conv o a) C)) ctxt
+            val goal_rewrite =
+                t_conv arg1_conv (mset_regroup_conv iqs)
+                then_conv t_conv arg_conv (mset_regroup_conv ips)
+            end
+          in
+            CONVERSION goal_rewrite 1
+            THEN (if strict then rtac smsI' 1
+                  else if qs = lq then rtac wmsI2'' 1
+                  else rtac wmsI1 1)
+            THEN mset_pwleq_tac 1
+            THEN EVERY (map2 (less_proof false) qs ps)
+            THEN (if strict orelse qs <> lq
+                  then LocalDefs.unfold_tac ctxt set_of_simps
+                       THEN steps_tac MAX true (lq \\ qs) (lp \\ ps)
+                  else all_tac)
+          end
+      in
+        rem_inv_img ctxt
+        THEN steps_tac label strict (nth lev q) (nth lev p)
+      end
+
+    val (mk_set, setT) = if label = MS then (mk_mset, msetT) else (mk_set, setT)
+
+    fun tag_pair p (i, tag) =
+      HOLogic.pair_const natT natT $
+        (measure_fn p i $ Bound 0) $ HOLogic.mk_number natT tag
+
+    fun pt_lev (p, lm) = Abs ("x", Termination.get_types D p,
+                           mk_set nat_pairT (map (tag_pair p) lm))
+
+    val level_mapping =
+      map_index pt_lev lev
+        |> Termination.mk_sumcases D (setT nat_pairT)
+        |> cterm_of thy
+    in
+      PROFILE "Proof Reconstruction"
+        (CONVERSION (Conv.arg_conv (Conv.arg_conv (FundefLib.regroup_union_conv sl))) 1
+         THEN (rtac @{thm reduction_pair_lemma} 1)
+         THEN (rtac @{thm rp_inv_image_rp} 1)
+         THEN (rtac (order_rpair ms_rp label) 1)
+         THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
+         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of thy)
+         THEN LocalDefs.unfold_tac ctxt
+           (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
+         THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
+         THEN EVERY (map (prove_lev true) sl)
+         THEN EVERY (map (prove_lev false) ((0 upto length cs - 1) \\ sl)))
+    end
+
+
+
+local open Termination in
+fun print_cell (SOME (Less _)) = "<"
+  | print_cell (SOME (LessEq _)) = "\<le>"
+  | print_cell (SOME (None _)) = "-"
+  | print_cell (SOME (False _)) = "-"
+  | print_cell (NONE) = "?"
+
+fun print_error ctxt D = CALLS (fn (cs, i) =>
+  let
+    val np = get_num_points D
+    val ms = map (get_measures D) (0 upto np - 1)
+    val tys = map (get_types D) (0 upto np - 1)
+    fun index xs = (1 upto length xs) ~~ xs
+    fun outp s t f xs = map (fn (x, y) => s ^ Int.toString x ^ t ^ f y ^ "\n") xs
+    val ims = index (map index ms)
+    val _ = Output.tracing (concat (outp "fn #" ":\n" (concat o outp "\tmeasure #" ": " (Syntax.string_of_term ctxt)) ims))
+    fun print_call (k, c) =
+      let
+        val (_, p, _, q, _, _) = dest_call D c
+        val _ = Output.tracing ("call table for call #" ^ Int.toString k ^ ": fn " ^ 
+                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1))
+        val caller_ms = nth ms p
+        val callee_ms = nth ms q
+        val entries = map (fn x => map (pair x) (callee_ms)) (caller_ms)
+        fun print_ln (i : int, l) = concat (Int.toString i :: "   " :: map (enclose " " " " o print_cell o (uncurry (get_descent D c))) l)
+        val _ = Output.tracing (concat (Int.toString (p + 1) ^ "|" ^ Int.toString (q + 1) ^ 
+                                        " " :: map (enclose " " " " o Int.toString) (1 upto length callee_ms)) ^ "\n" 
+                                ^ cat_lines (map print_ln ((1 upto (length entries)) ~~ entries)))
+      in
+        true
+      end
+    fun list_call (k, c) =
+      let
+        val (_, p, _, q, _, _) = dest_call D c
+        val _ = Output.tracing ("call #" ^ (Int.toString k) ^ ": fn " ^
+                                Int.toString (p + 1) ^ " ~> fn " ^ Int.toString (q + 1) ^ "\n" ^ 
+                                (Syntax.string_of_term ctxt c))
+      in true end
+    val _ = forall list_call ((1 upto length cs) ~~ cs)
+    val _ = forall print_call ((1 upto length cs) ~~ cs)
+  in
+    all_tac
+  end)
+end
+
+
+fun single_scnp_tac use_tags orders ctxt cont err_cont D = Termination.CALLS (fn (cs, i) =>
+  let
+    val gp = gen_probl D cs
+(*    val _ = TRACE ("SCNP instance: " ^ makestring gp)*)
+    val certificate = generate_certificate use_tags orders gp
+(*    val _ = TRACE ("Certificate: " ^ makestring certificate)*)
+
+    val ms_configured = is_some (MultisetSetup.get (ProofContext.theory_of ctxt))
+    in
+    case certificate
+     of NONE => err_cont D i
+      | SOME cert =>
+        if not ms_configured andalso #1 cert = MS
+        then err_cont D i
+        else SELECT_GOAL (reconstruct_tac ctxt D cs gp cert) i
+             THEN (rtac @{thm wf_empty} i ORELSE cont D i)
+  end)
+
+fun decomp_scnp_tac orders autom_tac ctxt err_cont =
+  let
+    open Termination
+    val derive_diag = Descent.derive_diag ctxt autom_tac
+    val derive_all = Descent.derive_all ctxt autom_tac
+    val decompose = Decompose.decompose_tac ctxt autom_tac
+    val scnp_no_tags = single_scnp_tac false orders ctxt
+    val scnp_full = single_scnp_tac true orders ctxt
+
+    fun first_round c e =
+        derive_diag (REPEAT scnp_no_tags c e)
+
+    val second_round =
+        REPEAT (fn c => fn e => decompose (scnp_no_tags c c) e)
+
+    val third_round =
+        derive_all oo
+        REPEAT (fn c => fn e =>
+          scnp_full (decompose c c) e)
+
+    fun Then s1 s2 c e = s1 (s2 c c) (s2 c e)
+
+    val strategy = Then (Then first_round second_round) third_round
+
+  in
+    TERMINATION ctxt (strategy err_cont err_cont)
+  end
+
+fun decomp_scnp orders ctxt =
+  let
+    val extra_simps = FundefCommon.TerminationSimps.get ctxt
+    val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
+  in
+    Method.SIMPLE_METHOD
+      (TRY (FundefCommon.apply_termination_rule ctxt 1)
+       THEN TRY Termination.wf_union_tac
+       THEN
+         (rtac @{thm wf_empty} 1
+          ORELSE decomp_scnp_tac orders autom_tac ctxt (print_error ctxt) 1))
+  end
+
+
+(* Method setup *)
+
+val orders =
+  (Scan.repeat1
+    ((Args.$$$ "max" >> K MAX) ||
+     (Args.$$$ "min" >> K MIN) ||
+     (Args.$$$ "ms" >> K MS))
+  || Scan.succeed [MAX, MS, MIN])
+
+val setup = Method.add_method
+  ("sizechange", Method.sectioned_args (Scan.lift orders) clasimp_modifiers decomp_scnp,
+   "termination prover with graph decomposition and the NP subset of size change termination")
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/scnp_solve.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/scnp_solve.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,257 @@
+(*  Title:       HOL/Tools/function_package/scnp_solve.ML
+    Author:      Armin Heller, TU Muenchen
+    Author:      Alexander Krauss, TU Muenchen
+
+Generate certificates for SCNP using a SAT solver
+*)
+
+
+signature SCNP_SOLVE =
+sig
+
+  datatype edge = GTR | GEQ
+  datatype graph = G of int * int * (int * edge * int) list
+  datatype graph_problem = GP of int list * graph list
+
+  datatype label = MIN | MAX | MS
+
+  type certificate =
+    label                   (* which order *)
+    * (int * int) list list (* (multi)sets *)
+    * int list              (* strictly ordered calls *)
+    * (int -> bool -> int -> (int * int) option) (* covering function *)
+
+  val generate_certificate : bool -> label list -> graph_problem -> certificate option
+
+  val solver : string ref
+end
+
+structure ScnpSolve : SCNP_SOLVE =
+struct
+
+(** Graph problems **)
+
+datatype edge = GTR | GEQ ;
+datatype graph = G of int * int * (int * edge * int) list ;
+datatype graph_problem = GP of int list * graph list ;
+
+datatype label = MIN | MAX | MS ;
+type certificate =
+  label
+  * (int * int) list list
+  * int list
+  * (int -> bool -> int -> (int * int) option)
+
+fun graph_at (GP (_, gs), i) = nth gs i ;
+fun num_prog_pts (GP (arities, _)) = length arities ;
+fun num_graphs (GP (_, gs)) = length gs ;
+fun arity (GP (arities, gl)) i = nth arities i ;
+fun ndigits (GP (arities, _)) = IntInf.log2 (foldl (op +) 0 arities) + 1
+
+
+(** Propositional formulas **)
+
+val Not = PropLogic.Not and And = PropLogic.And and Or = PropLogic.Or
+val BoolVar = PropLogic.BoolVar
+fun Implies (p, q) = Or (Not p, q)
+fun Equiv (p, q) = And (Implies (p, q), Implies (q, p))
+val all = PropLogic.all
+
+(* finite indexed quantifiers:
+
+iforall n f   <==>      /\
+                       /  \  f i
+                      0<=i<n
+ *)
+fun iforall n f = all (map f (0 upto n - 1))
+fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
+
+fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun exactly_one n f = iexists n (the_one f n)
+
+(* SAT solving *)
+val solver = ref "auto";
+fun sat_solver x =
+  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+
+(* "Virtual constructors" for various propositional variables *)
+fun var_constrs (gp as GP (arities, gl)) =
+  let
+    val n = Int.max (num_graphs gp, num_prog_pts gp)
+    val k = foldl Int.max 1 arities
+
+    (* Injective, provided  a < 8, x < n, and i < k. *)
+    fun prod a x i j = ((j * k + i) * n + x) * 8 + a + 1
+
+    fun ES (g, i, j) = BoolVar (prod 0 g i j)
+    fun EW (g, i, j) = BoolVar (prod 1 g i j)
+    fun WEAK g       = BoolVar (prod 2 g 0 0)
+    fun STRICT g     = BoolVar (prod 3 g 0 0)
+    fun P (p, i)     = BoolVar (prod 4 p i 0)
+    fun GAM (g, i, j)= BoolVar (prod 5 g i j)
+    fun EPS (g, i)   = BoolVar (prod 6 g i 0)
+    fun TAG (p, i) b = BoolVar (prod 7 p i b)
+  in
+    (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG)
+  end
+
+
+fun graph_info gp g =
+  let
+    val G (p, q, edgs) = graph_at (gp, g)
+  in
+    (g, p, q, arity gp p, arity gp q, edgs)
+  end
+
+
+(* Order-independent part of encoding *)
+
+fun encode_graphs bits gp =
+  let
+    val ng = num_graphs gp
+    val (ES,EW,_,_,_,_,_,TAG) = var_constrs gp
+
+    fun encode_constraint_strict 0 (x, y) = PropLogic.False
+      | encode_constraint_strict k (x, y) =
+        Or (And (TAG x (k - 1), Not (TAG y (k - 1))),
+            And (Equiv (TAG x (k - 1), TAG y (k - 1)),
+                 encode_constraint_strict (k - 1) (x, y)))
+
+    fun encode_constraint_weak k (x, y) =
+        Or (encode_constraint_strict k (x, y),
+            iforall k (fn i => Equiv (TAG x i, TAG y i)))
+
+    fun encode_graph (g, p, q, n, m, edges) =
+      let
+        fun encode_edge i j =
+          if exists (fn x => x = (i, GTR, j)) edges then
+            And (ES (g, i, j), EW (g, i, j))
+          else if not (exists (fn x => x = (i, GEQ, j)) edges) then
+            And (Not (ES (g, i, j)), Not (EW (g, i, j)))
+          else
+            And (
+              Equiv (ES (g, i, j),
+                     encode_constraint_strict bits ((p, i), (q, j))),
+              Equiv (EW (g, i, j),
+                     encode_constraint_weak bits ((p, i), (q, j))))
+       in
+        iforall2 n m encode_edge
+      end
+  in
+    iforall ng (encode_graph o graph_info gp)
+  end
+
+
+(* Order-specific part of encoding *)
+
+fun encode bits gp mu =
+  let
+    val ng = num_graphs gp
+    val (ES,EW,WEAK,STRICT,P,GAM,EPS,_) = var_constrs gp
+
+    fun encode_graph MAX (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i =>
+                  And (P (p, i), EW (g, i, j)))))),
+          Equiv (STRICT g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i =>
+                  And (P (p, i), ES (g, i, j)))))),
+          iexists n (fn i => P (p, i))
+        ]
+      | encode_graph MIN (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall n (fn i =>
+              Implies (P (p, i),
+                iexists m (fn j =>
+                  And (P (q, j), EW (g, i, j)))))),
+          Equiv (STRICT g,
+            iforall n (fn i =>
+              Implies (P (p, i),
+                iexists m (fn j =>
+                  And (P (q, j), ES (g, i, j)))))),
+          iexists m (fn j => P (q, j))
+        ]
+      | encode_graph MS (g, p, q, n, m, _) =
+        all [
+          Equiv (WEAK g,
+            iforall m (fn j =>
+              Implies (P (q, j),
+                iexists n (fn i => GAM (g, i, j))))),
+          Equiv (STRICT g,
+            iexists n (fn i =>
+              And (P (p, i), Not (EPS (g, i))))),
+          iforall2 n m (fn i => fn j =>
+            Implies (GAM (g, i, j),
+              all [
+                P (p, i),
+                P (q, j),
+                EW (g, i, j),
+                Equiv (Not (EPS (g, i)), ES (g, i, j))])),
+          iforall n (fn i =>
+            Implies (And (P (p, i), EPS (g, i)),
+              exactly_one m (fn j => GAM (g, i, j))))
+        ]
+  in
+    all [
+      encode_graphs bits gp,
+      iforall ng (encode_graph mu o graph_info gp),
+      iforall ng (fn x => WEAK x),
+      iexists ng (fn x => STRICT x)
+    ]
+  end
+
+
+(*Generieren des level-mapping und diverser output*)
+fun mk_certificate bits label gp f =
+  let
+    val (ES,EW,WEAK,STRICT,P,GAM,EPS,TAG) = var_constrs gp
+    fun assign (PropLogic.BoolVar v) = the_default false (f v)
+    fun assignTag i j =
+      (fold (fn x => fn y => 2 * y + (if assign (TAG (i, j) x) then 1 else 0))
+        (bits - 1 downto 0) 0)
+
+    val level_mapping =
+      let fun prog_pt_mapping p =
+            map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
+              (0 upto (arity gp p) - 1)
+      in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+
+    val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)
+
+    fun covering_pair g bStrict j =
+      let
+        val (_, p, q, n, m, _) = graph_info gp g
+
+        fun cover        MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (EW  (g, i, j))) (0 upto n - 1)
+          | cover        MS  k = find_index (fn i =>                                     assign (GAM (g, i, k))) (0 upto n - 1)
+          | cover        MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (EW  (g, i, j))) (0 upto m - 1)
+        fun cover_strict MAX j = find_index (fn i => assign (P (p, i))      andalso      assign (ES  (g, i, j))) (0 upto n - 1)
+          | cover_strict MS  k = find_index (fn i => assign (GAM (g, i, k)) andalso not (assign (EPS (g, i)  ))) (0 upto n - 1)
+          | cover_strict MIN i = find_index (fn j => assign (P (q, j))      andalso      assign (ES  (g, i, j))) (0 upto m - 1)
+        val i = if bStrict then cover_strict label j else cover label j
+      in
+        find_first (fn x => fst x = i) (nth level_mapping (if label = MIN then q else p))
+      end
+  in
+    (label, level_mapping, strict_list, covering_pair)
+  end
+
+(*interface for the proof reconstruction*)
+fun generate_certificate use_tags labels gp =
+  let
+    val bits = if use_tags then ndigits gp else 0
+  in
+    get_first
+      (fn l => case sat_solver (encode bits gp l) of
+                 SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
+               | _ => NONE)
+      labels
+  end
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Tools/function_package/termination.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/function_package/termination.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,324 @@
+(*  Title:       HOL/Tools/function_package/termination_data.ML
+    Author:      Alexander Krauss, TU Muenchen
+
+Context data for termination proofs
+*)
+
+
+signature TERMINATION =
+sig
+
+  type data
+  datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm
+
+  val mk_sumcases : data -> typ -> term list -> term
+
+  val note_measure : int -> term -> data -> data
+  val note_chain   : term -> term -> thm option -> data -> data
+  val note_descent : term -> term -> term -> cell -> data -> data
+
+  val get_num_points : data -> int
+  val get_types      : data -> int -> typ
+  val get_measures   : data -> int -> term list
+
+  (* read from cache *)
+  val get_chain      : data -> term -> term -> thm option option
+  val get_descent    : data -> term -> term -> term -> cell option
+
+  (* writes *)
+  val derive_descent  : theory -> tactic -> term -> term -> term -> data -> data
+  val derive_descents : theory -> tactic -> term -> data -> data
+
+  val dest_call : data -> term -> ((string * typ) list * int * term * int * term * term)
+
+  val CALLS : (term list * int -> tactic) -> int -> tactic
+
+  (* Termination tactics. Sequential composition via continuations. (2nd argument is the error continuation) *)
+  type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+  val TERMINATION : Proof.context -> (data -> int -> tactic) -> int -> tactic
+
+  val REPEAT : ttac -> ttac
+
+  val wf_union_tac : tactic
+end
+
+
+
+structure Termination : TERMINATION =
+struct
+
+open FundefLib
+
+val term2_ord = prod_ord Term.fast_term_ord Term.fast_term_ord
+structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
+structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord Term.fast_term_ord term2_ord);
+
+(** Analyzing binary trees **)
+
+(* Skeleton of a tree structure *)
+
+datatype skel =
+  SLeaf of int (* index *)
+| SBranch of (skel * skel)
+
+
+(* abstract make and dest functions *)
+fun mk_tree leaf branch =
+  let fun mk (SLeaf i) = leaf i
+        | mk (SBranch (s, t)) = branch (mk s, mk t)
+  in mk end
+
+
+fun dest_tree split =
+  let fun dest (SLeaf i) x = [(i, x)]
+        | dest (SBranch (s, t)) x =
+          let val (l, r) = split x
+          in dest s l @ dest t r end
+  in dest end
+
+
+(* concrete versions for sum types *)
+fun is_inj (Const ("Sum_Type.Inl", _) $ _) = true
+  | is_inj (Const ("Sum_Type.Inr", _) $ _) = true
+  | is_inj _ = false
+
+fun dest_inl (Const ("Sum_Type.Inl", _) $ t) = SOME t
+  | dest_inl _ = NONE
+
+fun dest_inr (Const ("Sum_Type.Inr", _) $ t) = SOME t
+  | dest_inr _ = NONE
+
+
+fun mk_skel ps =
+  let
+    fun skel i ps =
+      if forall is_inj ps andalso not (null ps)
+      then let
+          val (j, s) = skel i (map_filter dest_inl ps)
+          val (k, t) = skel j (map_filter dest_inr ps)
+        in (k, SBranch (s, t)) end
+      else (i + 1, SLeaf i)
+  in
+    snd (skel 0 ps)
+  end
+
+(* compute list of types for nodes *)
+fun node_types sk T = dest_tree (fn Type ("+", [LT, RT]) => (LT, RT)) sk T |> map snd
+
+(* find index and raw term *)
+fun dest_inj (SLeaf i) trm = (i, trm)
+  | dest_inj (SBranch (s, t)) trm =
+    case dest_inl trm of
+      SOME trm' => dest_inj s trm'
+    | _ => dest_inj t (the (dest_inr trm))
+
+
+
+(** Matrix cell datatype **)
+
+datatype cell = Less of thm | LessEq of (thm * thm) | None of (thm * thm) | False of thm;
+
+
+type data =
+  skel                            (* structure of the sum type encoding "program points" *)
+  * (int -> typ)                  (* types of program points *)
+  * (term list Inttab.table)      (* measures for program points *)
+  * (thm option Term2tab.table)   (* which calls form chains? *)
+  * (cell Term3tab.table)         (* local descents *)
+
+
+fun map_measures f (p, T, M, C, D) = (p, T, f M, C, D)
+fun map_chains f   (p, T, M, C, D) = (p, T, M, f C, D)
+fun map_descent f  (p, T, M, C, D) = (p, T, M, C, f D)
+
+fun note_measure p m = map_measures (Inttab.insert_list (op aconv) (p, m))
+fun note_chain c1 c2 res = map_chains (Term2tab.update ((c1, c2), res))
+fun note_descent c m1 m2 res = map_descent (Term3tab.update ((c,(m1, m2)), res))
+
+(* Build case expression *)
+fun mk_sumcases (sk, _, _, _, _) T fs =
+  mk_tree (fn i => (nth fs i, domain_type (fastype_of (nth fs i))))
+          (fn ((f, fT), (g, gT)) => (SumTree.mk_sumcase fT gT T f g, SumTree.mk_sumT fT gT))
+          sk
+  |> fst
+
+fun mk_sum_skel rel =
+  let
+    val cs = FundefLib.dest_binop_list @{const_name "op Un"} rel
+    fun collect_pats (Const ("Collect", _) $ Abs (_, _, c)) =
+      let
+        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+          = Term.strip_qnt_body "Ex" c
+      in cons r o cons l end
+  in
+    mk_skel (fold collect_pats cs [])
+  end
+
+fun create ctxt T rel =
+  let
+    val sk = mk_sum_skel rel
+    val Ts = node_types sk T
+    val M = Inttab.make (map_index (apsnd (MeasureFunctions.get_measure_functions ctxt)) Ts)
+  in
+    (sk, nth Ts, M, Term2tab.empty, Term3tab.empty)
+  end
+
+fun get_num_points (sk, _, _, _, _) =
+  let
+    fun num (SLeaf i) = i + 1
+      | num (SBranch (s, t)) = num t
+  in num sk end
+
+fun get_types (_, T, _, _, _) = T
+fun get_measures (_, _, M, _, _) = Inttab.lookup_list M
+
+fun get_chain (_, _, _, C, _) c1 c2 =
+  Term2tab.lookup C (c1, c2)
+
+fun get_descent (_, _, _, _, D) c m1 m2 =
+  Term3tab.lookup D (c, (m1, m2))
+
+fun dest_call D (Const ("Collect", _) $ Abs (_, _, c)) =
+  let
+    val n = get_num_points D
+    val (sk, _, _, _, _) = D
+    val vs = Term.strip_qnt_vars "Ex" c
+
+    (* FIXME: throw error "dest_call" for malformed terms *)
+    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+      = Term.strip_qnt_body "Ex" c
+    val (p, l') = dest_inj sk l
+    val (q, r') = dest_inj sk r
+  in
+    (vs, p, l', q, r', Gam)
+  end
+  | dest_call D t = error "dest_call"
+
+
+fun derive_desc_aux thy tac c (vs, p, l', q, r', Gam) m1 m2 D =
+  case get_descent D c m1 m2 of
+    SOME _ => D
+  | NONE => let
+    fun cgoal rel =
+      Term.list_all (vs,
+        Logic.mk_implies (HOLogic.mk_Trueprop Gam,
+          HOLogic.mk_Trueprop (Const (rel, @{typ "nat => nat => bool"})
+            $ (m2 $ r') $ (m1 $ l'))))
+      |> cterm_of thy
+    in
+      note_descent c m1 m2
+        (case try_proof (cgoal @{const_name HOL.less}) tac of
+           Solved thm => Less thm
+         | Stuck thm =>
+           (case try_proof (cgoal @{const_name HOL.less_eq}) tac of
+              Solved thm2 => LessEq (thm2, thm)
+            | Stuck thm2 =>
+              if prems_of thm2 = [HOLogic.Trueprop $ HOLogic.false_const]
+              then False thm2 else None (thm2, thm)
+            | _ => raise Match) (* FIXME *)
+         | _ => raise Match) D
+      end
+
+fun derive_descent thy tac c m1 m2 D =
+  derive_desc_aux thy tac c (dest_call D c) m1 m2 D
+
+(* all descents in one go *)
+fun derive_descents thy tac c D =
+  let val cdesc as (vs, p, l', q, r', Gam) = dest_call D c
+  in fold_product (derive_desc_aux thy tac c cdesc)
+       (get_measures D p) (get_measures D q) D
+  end
+
+fun CALLS tac i st =
+  if Thm.no_prems st then all_tac st
+  else case Thm.term_of (Thm.cprem_of st i) of
+    (_ $ (_ $ rel)) => tac (FundefLib.dest_binop_list @{const_name "op Un"} rel, i) st
+  |_ => no_tac st
+
+type ttac = (data -> int -> tactic) -> (data -> int -> tactic) -> data -> int -> tactic
+
+fun TERMINATION ctxt tac =
+  SUBGOAL (fn (_ $ (Const (@{const_name "wf"}, wfT) $ rel), i) =>
+  let
+    val (T, _) = HOLogic.dest_prodT (HOLogic.dest_setT (domain_type wfT))
+  in
+    tac (create ctxt T rel) i
+  end)
+
+
+(* A tactic to convert open to closed termination goals *)
+local
+fun dest_term (t : term) = (* FIXME, cf. Lexicographic order *)
+    let
+      val (vars, prop) = FundefLib.dest_all_all t
+      val (prems, concl) = Logic.strip_horn prop
+      val (lhs, rhs) = concl
+                         |> HOLogic.dest_Trueprop
+                         |> HOLogic.dest_mem |> fst
+                         |> HOLogic.dest_prod
+    in
+      (vars, prems, lhs, rhs)
+    end
+
+fun mk_pair_compr (T, qs, l, r, conds) =
+    let
+      val pT = HOLogic.mk_prodT (T, T)
+      val n = length qs
+      val peq = HOLogic.eq_const pT $ Bound n $ (HOLogic.pair_const T T $ l $ r)
+      val conds' = if null conds then [HOLogic.true_const] else conds
+    in
+      HOLogic.Collect_const pT $
+      Abs ("uu_", pT,
+           (foldr1 HOLogic.mk_conj (peq :: conds')
+            |> fold_rev (fn v => fn t => HOLogic.exists_const (fastype_of v) $ lambda v t) qs))
+    end
+
+in
+
+fun wf_union_tac st =
+    let
+      val thy = theory_of_thm st
+      val cert = cterm_of (theory_of_thm st)
+      val ((trueprop $ (wf $ rel)) :: ineqs) = prems_of st
+
+      fun mk_compr ineq =
+          let
+            val (vars, prems, lhs, rhs) = dest_term ineq
+          in
+            mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+          end
+
+      val relation =
+          if null ineqs then
+              Const (@{const_name "{}"}, fastype_of rel)
+          else
+              foldr1 (HOLogic.mk_binop @{const_name "op Un"}) (map mk_compr ineqs)
+
+      fun solve_membership_tac i =
+          (EVERY' (replicate (i - 2) (rtac @{thm UnI2}))  (* pick the right component of the union *)
+          THEN' (fn j => TRY (rtac @{thm UnI1} j))
+          THEN' (rtac @{thm CollectI})                    (* unfold comprehension *)
+          THEN' (fn i => REPEAT (rtac @{thm exI} i))      (* Turn existentials into schematic Vars *)
+          THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
+                 ORELSE' ((rtac @{thm conjI})
+                          THEN' (rtac @{thm refl})
+                          THEN' (CLASET' blast_tac)))     (* Solve rest of context... not very elegant *)
+          ) i
+    in
+      ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
+      THEN ALLGOALS (fn i => if i = 1 then all_tac else solve_membership_tac i))) st
+    end
+
+
+end
+
+
+(* continuation passing repeat combinator *)
+fun REPEAT ttac cont err_cont =
+    ttac (fn D => fn i => (REPEAT ttac cont cont D i)) err_cont
+
+
+
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/Wellfounded.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -842,6 +842,11 @@
   qed
 qed
 
+lemma max_ext_additive: 
+ "(A, B) \<in> max_ext R \<Longrightarrow> (C, D) \<in> max_ext R \<Longrightarrow>
+  (A \<union> C, B \<union> D) \<in> max_ext R"
+by (force elim!: max_ext.cases)
+
 
 definition
   min_ext :: "('a \<times> 'a) set \<Rightarrow> ('a set \<times> 'a set) set" 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/ex/CodegenSML_Test.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/CodegenSML_Test.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -0,0 +1,54 @@
+(*  Title:      Test file for Stefan Berghofer's SML code generator
+    Author:     Tobias Nipkow, TU Muenchen
+*)
+
+theory CodegenSML_Test
+imports Executable_Set
+begin
+
+lemma "True : {False, True} & False ~: {True}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} \<union> {3,1,2,1}) {2,2,3,1} &
+ eq_set ({1::nat,2,3,2} \<union> {4,1,5,1}) {4,4,5,1,2,3}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} \<inter> {3,1,2,1}) {2,2,3,1} & 
+ eq_set ({1::nat,2,3,2} \<inter> {4,1,5,2}) {2,1,2}"
+by evaluation
+
+lemma
+"eq_set ({1::nat,2,3,2} - {3,1,2,1}) {} & 
+ eq_set ({1::nat,2,3,2} - {4,1,5,2}) {3}"
+by evaluation
+
+lemma
+"eq_set (Union{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} &
+ eq_set (Union{{1::nat,2,3,2}, {4,1,5,1}}) {4,4,5,1,2,3}"
+by evaluation
+
+lemma
+"eq_set (Inter{{1::nat,2,3,2}, {3,1,2,1}}) {2,2,3,1} & 
+ eq_set (Inter{{1::nat,2,3,2}, {4,1,5,2}}) {2,1,2}"
+by evaluation
+
+lemma "eq_set ((%x. x+2) ` {1::nat,2,3,2}) {4,5,3,3}"
+by evaluation
+
+lemma
+"(ALL x:{1::nat,2,3,2}. EX y : {4,5,2}. x < y) &
+ (EX x:{1::nat,2,3,2}. ALL y : {4,5,6}. x < y)"
+by evaluation
+
+lemma
+"eq_set {x : {4::nat,7,10}. 2 dvd x } {4,10}"
+by evaluation
+
+lemma
+"fold (op +) (5::int) {3,7,9} = 24 &
+ fold_image (op *) id (2::int) {3,4,5} = 120"
+by evaluation
+
+end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/HOL/ex/ExecutableContent.thy	Tue Dec 16 21:18:53 2008 -0800
@@ -24,4 +24,11 @@
   "~~/src/HOL/ex/Records"
 begin
 
+text {* However, some aren't executable *}
+
+declare pair_leq_def[code del]
+declare max_weak_def[code del]
+declare min_weak_def[code del]
+declare ms_weak_def[code del]
+
 end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Concurrent/ROOT.ML
--- a/src/Pure/Concurrent/ROOT.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Concurrent/ROOT.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,15 +1,12 @@
 (*  Title:      Pure/Concurrent/ROOT.ML
-    ID:         $Id$
+    Author:     Makarius
 
 Concurrency within the ML runtime.
 *)
 
-val future_scheduler = ref true;
-
 use "simple_thread.ML";
 use "synchronized.ML";
 use "mailbox.ML";
-use "schedule.ML";
 use "task_queue.ML";
 use "future.ML";
 use "par_list.ML";
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Concurrent/future.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Concurrent/future.ML
-    ID:         $Id$
     Author:     Makarius
 
 Future values.
@@ -28,8 +27,8 @@
 signature FUTURE =
 sig
   val enabled: unit -> bool
-  type task = TaskQueue.task
-  type group = TaskQueue.group
+  type task = Task_Queue.task
+  type group = Task_Queue.group
   val thread_data: unit -> (string * task) option
   type 'a future
   val task_of: 'a future -> task
@@ -40,12 +39,11 @@
   val fork: (unit -> 'a) -> 'a future
   val fork_group: group -> (unit -> 'a) -> 'a future
   val fork_deps: 'b future list -> (unit -> 'a) -> 'a future
-  val fork_background: (unit -> 'a) -> 'a future
+  val fork_pri: int -> (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val focus: task list -> unit
   val interrupt_task: string -> unit
   val cancel: 'a future -> unit
   val shutdown: unit -> unit
@@ -57,14 +55,14 @@
 (** future values **)
 
 fun enabled () =
-  ! future_scheduler andalso Multithreading.enabled () andalso
+  Multithreading.enabled () andalso
     not (Multithreading.self_critical ());
 
 
 (* identifiers *)
 
-type task = TaskQueue.task;
-type group = TaskQueue.group;
+type task = Task_Queue.task;
+type group = Task_Queue.group;
 
 local val tag = Universal.tag () : (string * task) option Universal.tag in
   fun thread_data () = the_default NONE (Thread.getLocal tag);
@@ -86,8 +84,8 @@
 fun is_finished x = is_some (peek x);
 
 fun value x = Future
- {task = TaskQueue.new_task (),
-  group = TaskQueue.new_group (),
+ {task = Task_Queue.new_task 0,
+  group = Task_Queue.new_group (),
   result = ref (SOME (Exn.Result x))};
 
 
@@ -96,12 +94,12 @@
 
 (* global state *)
 
-val queue = ref TaskQueue.empty;
+val queue = ref Task_Queue.empty;
 val next = ref 0;
 val workers = ref ([]: (Thread.thread * bool) list);
 val scheduler = ref (NONE: Thread.thread option);
 val excessive = ref 0;
-val canceled = ref ([]: TaskQueue.group list);
+val canceled = ref ([]: Task_Queue.group list);
 val do_shutdown = ref false;
 
 
@@ -114,15 +112,11 @@
 
 fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
 
-fun wait name = (*requires SYNCHRONIZED*)
- (Multithreading.tracing 3 (fn () => name ^ ": wait ...");
+fun wait () = (*requires SYNCHRONIZED*)
   ConditionVar.wait (cond, lock);
-  Multithreading.tracing 3 (fn () => name ^ ": ... continue"));
 
-fun wait_timeout name timeout = (*requires SYNCHRONIZED*)
- (Multithreading.tracing 3 (fn () => name ^ ": wait ...");
+fun wait_timeout timeout = (*requires SYNCHRONIZED*)
   ConditionVar.waitUntil (cond, lock, Time.+ (Time.now (), timeout));
-  Multithreading.tracing 3 (fn () => name ^ ": ... continue"));
 
 fun notify_all () = (*requires SYNCHRONIZED*)
   ConditionVar.broadcast cond;
@@ -150,9 +144,9 @@
     val _ = trace_active ();
     val ok = setmp_thread_data (name, task) run ();
     val _ = SYNCHRONIZED "execute" (fn () =>
-     (change queue (TaskQueue.finish task);
+     (change queue (Task_Queue.finish task);
       if ok then ()
-      else if TaskQueue.cancel (! queue) group then ()
+      else if Task_Queue.cancel (! queue) group then ()
       else change canceled (cons group);
       notify_all ()));
   in () end;
@@ -160,23 +154,23 @@
 
 (* worker threads *)
 
-fun worker_wait name = (*requires SYNCHRONIZED*)
-  (change_active false; wait name; change_active true);
+fun worker_wait () = (*requires SYNCHRONIZED*)
+  (change_active false; wait (); change_active true);
 
-fun worker_next name = (*requires SYNCHRONIZED*)
+fun worker_next () = (*requires SYNCHRONIZED*)
   if ! excessive > 0 then
     (dec excessive;
      change workers (filter_out (fn (thread, _) => Thread.equal (thread, Thread.self ())));
      notify_all ();
      NONE)
   else
-    (case change_result queue TaskQueue.dequeue of
-      NONE => (worker_wait name; worker_next name)
+    (case change_result queue Task_Queue.dequeue of
+      NONE => (worker_wait (); worker_next ())
     | some => some);
 
 fun worker_loop name =
-  (case SYNCHRONIZED name (fn () => worker_next name) of
-    NONE => Multithreading.tracing 3 (fn () => name ^ ": exit")
+  (case SYNCHRONIZED name worker_next of
+    NONE => ()
   | SOME work => (execute name work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
@@ -204,27 +198,25 @@
       else ();
 
     (*canceled groups*)
-    val _ =  change canceled (filter_out (TaskQueue.cancel (! queue)));
+    val _ =  change canceled (filter_out (Task_Queue.cancel (! queue)));
 
     (*shutdown*)
     val continue = not (! do_shutdown andalso null (! workers));
     val _ = if continue then () else scheduler := NONE;
 
     val _ = notify_all ();
-    val _ = wait_timeout "scheduler" (Time.fromSeconds 3);
+    val _ = wait_timeout (Time.fromSeconds 3);
   in continue end;
 
 fun scheduler_loop () =
- (while SYNCHRONIZED "scheduler" scheduler_next do ();
-  Multithreading.tracing 3 (fn () => "scheduler: exit"));
+  while SYNCHRONIZED "scheduler" scheduler_next do ();
 
 fun scheduler_active () = (*requires SYNCHRONIZED*)
   (case ! scheduler of NONE => false | SOME thread => Thread.isActive thread);
 
 fun scheduler_check name = SYNCHRONIZED name (fn () =>
   if not (scheduler_active ()) then
-    (Multithreading.tracing 3 (fn () => "scheduler: fork");
-     do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
+    (do_shutdown := false; scheduler := SOME (SimpleThread.fork false scheduler_loop))
   else if ! do_shutdown then error "Scheduler shutdown in progress"
   else ());
 
@@ -235,7 +227,7 @@
   let
     val _ = scheduler_check "future check";
 
-    val group = (case opt_group of SOME group => group | NONE => TaskQueue.new_group ());
+    val group = (case opt_group of SOME group => group | NONE => Task_Queue.new_group ());
 
     val result = ref (NONE: 'a Exn.result option);
     val run = Multithreading.with_attributes (Thread.getAttributes ())
@@ -246,18 +238,18 @@
           val res_ok =
             (case res of
               Exn.Result _ => true
-            | Exn.Exn Exn.Interrupt => (TaskQueue.invalidate_group group; true)
+            | Exn.Exn Exn.Interrupt => (Task_Queue.invalidate_group group; true)
             | _ => false);
         in res_ok end);
 
     val task = SYNCHRONIZED "future" (fn () =>
-      change_result queue (TaskQueue.enqueue group deps pri run) before notify_all ());
+      change_result queue (Task_Queue.enqueue group deps pri run) before notify_all ());
   in Future {task = task, group = group, result = result} end;
 
-fun fork e = future NONE [] true e;
-fun fork_group group e = future (SOME group) [] true e;
-fun fork_deps deps e = future NONE (map task_of deps) true e;
-fun fork_background e = future NONE [] false e;
+fun fork e = future NONE [] 0 e;
+fun fork_group group e = future (SOME group) [] 0 e;
+fun fork_deps deps e = future NONE (map task_of deps) 0 e;
+fun fork_pri pri e = future NONE [] pri e;
 
 
 (* join: retrieve results *)
@@ -273,7 +265,7 @@
         fun join_loop _ [] = ()
           | join_loop name tasks =
               (case SYNCHRONIZED name (fn () =>
-                  change_result queue (TaskQueue.dequeue_towards tasks)) of
+                  change_result queue (Task_Queue.dequeue_towards tasks)) of
                 NONE => ()
               | SOME (work, tasks') => (execute name work; join_loop name tasks'));
         val _ =
@@ -281,18 +273,18 @@
             NONE =>
               (*alien thread -- refrain from contending for resources*)
               while exists (not o is_finished) xs
-              do SYNCHRONIZED "join_thread" (fn () => wait "join_thread")
+              do SYNCHRONIZED "join_thread" (fn () => wait ())
           | SOME (name, task) =>
               (*proper task -- actively work towards results*)
               let
                 val unfinished = xs |> map_filter
                   (fn Future {task, result = ref NONE, ...} => SOME task | _ => NONE);
                 val _ = SYNCHRONIZED "join" (fn () =>
-                  (change queue (TaskQueue.depend unfinished task); notify_all ()));
+                  (change queue (Task_Queue.depend unfinished task); notify_all ()));
                 val _ = join_loop ("join_loop: " ^ name) unfinished;
                 val _ =
                   while exists (not o is_finished) xs
-                  do SYNCHRONIZED "join_task" (fn () => worker_wait "join_task");
+                  do SYNCHRONIZED "join_task" (fn () => worker_wait ());
               in () end);
 
       in xs |> map (fn Future {result = ref (SOME res), ...} => res) end) ();
@@ -300,18 +292,16 @@
 fun join_result x = singleton join_results x;
 fun join x = Exn.release (join_result x);
 
-fun map f x = fork_deps [x] (fn () => f (join x));
+fun map f x =
+  let val task = task_of x
+  in future NONE [task] (Task_Queue.pri_of_task task) (fn () => f (join x)) end;
 
 
 (* misc operations *)
 
-(*focus: collection of high-priority task*)
-fun focus tasks = SYNCHRONIZED "focus" (fn () =>
-  change queue (TaskQueue.focus tasks));
-
 (*interrupt: permissive signal, may get ignored*)
 fun interrupt_task id = SYNCHRONIZED "interrupt"
-  (fn () => TaskQueue.interrupt_external (! queue) id);
+  (fn () => Task_Queue.interrupt_external (! queue) id);
 
 (*cancel: present and future group members will be interrupted eventually*)
 fun cancel x =
@@ -324,12 +314,12 @@
   if Multithreading.available then
    (scheduler_check "shutdown check";
     SYNCHRONIZED "shutdown" (fn () =>
-     (while not (scheduler_active ()) do wait "shutdown: scheduler inactive";
-      while not (TaskQueue.is_empty (! queue)) do wait "shutdown: join";
+     (while not (scheduler_active ()) do wait ();
+      while not (Task_Queue.is_empty (! queue)) do wait ();
       do_shutdown := true;
       notify_all ();
-      while not (null (! workers)) do wait "shutdown: workers";
-      while scheduler_active () do wait "shutdown: scheduler still active";
+      while not (null (! workers)) do wait ();
+      while scheduler_active () do wait ();
       OS.Process.sleep (Time.fromMilliseconds 300))))
   else ();
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Concurrent/par_list.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -30,7 +30,7 @@
 fun raw_map f xs =
   if Future.enabled () then
     let
-      val group = TaskQueue.new_group ();
+      val group = Task_Queue.new_group ();
       val futures = map (fn x => Future.fork_group group (fn () => f x)) xs;
       val _ = List.app (ignore o Future.join_result) futures;
     in Future.join_results futures end
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Concurrent/schedule.ML
--- a/src/Pure/Concurrent/schedule.ML	Tue Dec 16 09:44:59 2008 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(*  Title:      Pure/Concurrent/schedule.ML
-    ID:         $Id$
-    Author:     Makarius
-
-Scheduling -- multiple threads working on a queue of tasks.
-*)
-
-signature SCHEDULE =
-sig
-  datatype 'a task =
-    Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-  val schedule: int -> ('a -> 'a task * 'a) -> 'a -> exn list
-end;
-
-structure Schedule: SCHEDULE =
-struct
-
-datatype 'a task =
-  Task of {body: unit -> unit, cont: 'a -> 'a, fail: 'a -> 'a} | Wait | Terminate;
-
-fun schedule n next_task = uninterruptible (fn restore_attributes => fn tasks =>
-  let
-    (*synchronized execution*)
-    val lock = Mutex.mutex ();
-    fun SYNCHRONIZED e =
-      let
-        val _ = Mutex.lock lock;
-        val res = Exn.capture e ();
-        val _ = Mutex.unlock lock;
-      in Exn.release res end;
-
-    (*wakeup condition*)
-    val wakeup = ConditionVar.conditionVar ();
-    fun wakeup_all () = ConditionVar.broadcast wakeup;
-    fun wait () = ConditionVar.wait (wakeup, lock);
-    fun wait_timeout () =
-      ConditionVar.waitUntil (wakeup, lock, Time.+ (Time.now (), Time.fromSeconds 1));
-
-    (*queue of tasks*)
-    val queue = ref tasks;
-    val active = ref 0;
-    fun trace_active () = Multithreading.tracing 1 (fn () =>
-      "SCHEDULE: " ^ string_of_int (! active) ^ " active");
-    fun dequeue () =
-      (case change_result queue next_task of
-        Wait =>
-          (dec active; trace_active ();
-            wait ();
-            inc active; trace_active ();
-            dequeue ())
-      | next => next);
-
-    (*pool of running threads*)
-    val status = ref ([]: exn list);
-    val running = ref ([]: Thread.thread list);
-    fun start f = (inc active; change running (cons (SimpleThread.fork false f)));
-    fun stop () = (dec active; change running (remove Thread.equal (Thread.self ())));
-
-    (*worker thread*)
-    fun worker () =
-      (case SYNCHRONIZED dequeue of
-        Task {body, cont, fail} =>
-          (case Exn.capture (restore_attributes body) () of
-            Exn.Result () =>
-              (SYNCHRONIZED (fn () => (change queue cont; wakeup_all ())); worker ())
-          | Exn.Exn exn =>
-              SYNCHRONIZED (fn () =>
-                (change status (cons exn); change queue fail; stop (); wakeup_all ())))
-      | Terminate => SYNCHRONIZED (fn () => (stop (); wakeup_all ())));
-
-    (*main control: fork and wait*)
-    fun fork 0 = ()
-      | fork k = (start worker; fork (k - 1));
-    val _ = SYNCHRONIZED (fn () =>
-     (fork (Int.max (n, 1));
-      while not (null (! running)) do
-      (trace_active ();
-       if not (null (! status))
-       then (List.app SimpleThread.interrupt (! running))
-       else ();
-       wait_timeout ())));
-
-  in ! status end);
-
-end;
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Concurrent/task_queue.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Concurrent/task_queue.ML
-    ID:         $Id$
     Author:     Makarius
 
 Ordered queue of grouped tasks.
@@ -8,7 +7,8 @@
 signature TASK_QUEUE =
 sig
   eqtype task
-  val new_task: unit -> task
+  val new_task: int -> task
+  val pri_of_task: task -> int
   val str_of_task: task -> string
   eqtype group
   val new_group: unit -> group
@@ -17,9 +17,8 @@
   type queue
   val empty: queue
   val is_empty: queue -> bool
-  val enqueue: group -> task list -> bool -> (bool -> bool) -> queue -> task * queue
+  val enqueue: group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val depend: task list -> task -> queue -> queue
-  val focus: task list -> queue -> queue
   val dequeue: queue -> (task * group * (unit -> bool)) option * queue
   val dequeue_towards: task list -> queue ->
     (((task * group * (unit -> bool)) * task list) option * queue)
@@ -29,20 +28,27 @@
   val cancel: queue -> group -> bool
 end;
 
-structure TaskQueue: TASK_QUEUE =
+structure Task_Queue: TASK_QUEUE =
 struct
 
-(* identifiers *)
+(* tasks *)
+
+datatype task = Task of int * serial;
+fun new_task pri = Task (pri, serial ());
 
-datatype task = Task of serial;
-fun new_task () = Task (serial ());
+fun pri_of_task (Task (pri, _)) = pri;
+fun str_of_task (Task (_, i)) = string_of_int i;
 
-fun str_of_task (Task i) = string_of_int i;
+fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
+structure Task_Graph = GraphFun(type key = task val ord = task_ord);
 
 
+(* groups *)
+
 datatype group = Group of serial * bool ref;
 
 fun new_group () = Group (serial (), ref true);
+
 fun invalidate_group (Group (_, ok)) = ok := false;
 
 fun str_of_group (Group (i, ref ok)) =
@@ -52,50 +58,46 @@
 (* jobs *)
 
 datatype job =
-  Job of bool * (bool -> bool) |   (*priority, job: status -> status*)
+  Job of bool -> bool |
   Running of Thread.thread;
 
-type jobs = (group * job) IntGraph.T;
+type jobs = (group * job) Task_Graph.T;
 
-fun get_group (jobs: jobs) (Task id) = #1 (IntGraph.get_node jobs id);
-fun get_job (jobs: jobs) (Task id) = #2 (IntGraph.get_node jobs id);
-fun map_job (Task id) f (jobs: jobs) = IntGraph.map_node id (apsnd f) jobs;
+fun get_group (jobs: jobs) task = #1 (Task_Graph.get_node jobs task);
+fun get_job (jobs: jobs) task = #2 (Task_Graph.get_node jobs task);
+fun map_job task f (jobs: jobs) = Task_Graph.map_node task (apsnd f) jobs;
 
-fun add_job (Task id) (Task dep) (jobs: jobs) =
-  IntGraph.add_edge_acyclic (dep, id) jobs handle IntGraph.UNDEF _ => jobs;
+fun add_job task dep (jobs: jobs) =
+  Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
-fun check_job (jobs: jobs) (task as Task id) =
-  if can (IntGraph.get_node jobs) id then SOME task else NONE;
+fun add_job_acyclic task dep (jobs: jobs) =
+  Task_Graph.add_edge_acyclic (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
 
 (* queue of grouped jobs *)
 
 datatype queue = Queue of
  {groups: task list Inttab.table,   (*groups with presently active members*)
-  jobs: jobs,                       (*job dependency graph*)
-  focus: task list};                (*particular collection of high-priority tasks*)
+  jobs: jobs};                      (*job dependency graph*)
 
-fun make_queue groups jobs focus = Queue {groups = groups, jobs = jobs, focus = focus};
+fun make_queue groups jobs = Queue {groups = groups, jobs = jobs};
 
-val empty = make_queue Inttab.empty IntGraph.empty [];
-fun is_empty (Queue {jobs, ...}) = IntGraph.is_empty jobs;
+val empty = make_queue Inttab.empty Task_Graph.empty;
+fun is_empty (Queue {jobs, ...}) = Task_Graph.is_empty jobs;
 
 
 (* enqueue *)
 
-fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs, focus}) =
+fun enqueue (group as Group (gid, _)) deps pri job (Queue {groups, jobs}) =
   let
-    val task as Task id = new_task ();
+    val task = new_task pri;
     val groups' = Inttab.cons_list (gid, task) groups;
     val jobs' = jobs
-      |> IntGraph.new_node (id, (group, Job (pri, job))) |> fold (add_job task) deps;
-  in (task, make_queue groups' jobs' focus) end;
+      |> Task_Graph.new_node (task, (group, Job job)) |> fold (add_job task) deps;
+  in (task, make_queue groups' jobs') end;
 
-fun depend deps task (Queue {groups, jobs, focus}) =
-  make_queue groups (fold (add_job task) deps jobs) focus;
-
-fun focus tasks (Queue {groups, jobs, ...}) =
-  make_queue groups jobs (map_filter (check_job jobs) tasks);
+fun depend deps task (Queue {groups, jobs}) =
+  make_queue groups (fold (add_job_acyclic task) deps jobs);
 
 
 (* dequeue *)
@@ -103,38 +105,30 @@
 local
 
 fun dequeue_result NONE queue = (NONE, queue)
-  | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs, focus}) =
-      (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs) focus);
-
-fun dequeue_global req_pri (queue as Queue {jobs, ...}) =
-  let
-    fun ready (id, ((group as Group (_, ref ok), Job (pri, job)), ([], _))) =
-          if pri = req_pri then SOME (Task id, group, (fn () => job ok)) else NONE
-      | ready _ = NONE;
-  in dequeue_result (IntGraph.get_first ready jobs) queue end;
-
-fun dequeue_local focus (queue as Queue {jobs, ...}) =
-  let
-    fun ready id =
-      (case IntGraph.get_node jobs id of
-        (group as Group (_, ref ok), Job (_, job)) =>
-          if null (IntGraph.imm_preds jobs id) then SOME (Task id, group, (fn () => job ok))
-          else NONE
-      | _ => NONE);
-    val ids = map (fn Task id => id) focus;
-  in dequeue_result (get_first ready (IntGraph.all_preds jobs ids)) queue end;
+  | dequeue_result (SOME (result as (task, _, _))) (Queue {groups, jobs}) =
+      (SOME result, make_queue groups (map_job task (K (Running (Thread.self ()))) jobs));
 
 in
 
-fun dequeue (queue as Queue {focus, ...}) =
-  (case dequeue_local focus queue of
-    (NONE, _) =>
-      (case dequeue_global true queue of (NONE, _) => dequeue_global false queue | res => res)
-  | res => res);
+fun dequeue (queue as Queue {jobs, ...}) =
+  let
+    fun ready (task, ((group as Group (_, ref ok), Job job), ([], _))) =
+          SOME (task, group, (fn () => job ok))
+      | ready _ = NONE;
+  in dequeue_result (Task_Graph.get_first ready jobs) queue end;
 
 fun dequeue_towards tasks (queue as Queue {jobs, ...}) =
-  let val tasks' = map_filter (check_job jobs) tasks in
-    (case dequeue_local tasks' queue of
+  let
+    val tasks' = filter (can (Task_Graph.get_node jobs)) tasks;
+
+    fun ready task =
+      (case Task_Graph.get_node jobs task of
+        (group as Group (_, ref ok), Job job) =>
+          if null (Task_Graph.imm_preds jobs task) then SOME (task, group, (fn () => job ok))
+          else NONE
+      | _ => NONE);
+  in
+    (case dequeue_result (get_first ready (Task_Graph.all_preds jobs tasks')) queue of
       (NONE, queue') => (NONE, queue')
     | (SOME work, queue') => (SOME (work, tasks'), queue'))
   end;
@@ -147,8 +141,13 @@
 fun interrupt (Queue {jobs, ...}) task =
   (case try (get_job jobs) task of SOME (Running thread) => SimpleThread.interrupt thread | _ => ());
 
-fun interrupt_external queue str =
-  (case Int.fromString str of SOME id => interrupt queue (Task id) | NONE => ());
+fun interrupt_external (queue as Queue {jobs, ...}) str =
+  (case Int.fromString str of
+    SOME i =>
+      (case Task_Graph.get_first
+          (fn (task as Task (_, j), _) => if i = j then SOME task else NONE) jobs
+        of SOME task => interrupt queue task | NONE => ())
+  | NONE => ());
 
 
 (* misc operations *)
@@ -161,12 +160,11 @@
     val _ = List.app SimpleThread.interrupt running;
   in null running end;
 
-fun finish (task as Task id) (Queue {groups, jobs, focus}) =
+fun finish task (Queue {groups, jobs}) =
   let
     val Group (gid, _) = get_group jobs task;
     val groups' = Inttab.remove_list (op =) (gid, task) groups;
-    val jobs' = IntGraph.del_node id jobs;
-    val focus' = remove (op =) task focus;
-  in make_queue groups' jobs' focus' end;
+    val jobs' = Task_Graph.del_node task jobs;
+  in make_queue groups' jobs' end;
 
 end;
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/IsaMakefile	Tue Dec 16 21:18:53 2008 -0800
@@ -23,26 +23,24 @@
 
 $(OUT)/Pure: Concurrent/ROOT.ML Concurrent/future.ML			\
   Concurrent/mailbox.ML Concurrent/par_list.ML				\
-  Concurrent/par_list_dummy.ML Concurrent/schedule.ML			\
-  Concurrent/simple_thread.ML Concurrent/synchronized.ML		\
-  Concurrent/task_queue.ML General/ROOT.ML General/alist.ML		\
-  General/balanced_tree.ML General/basics.ML General/buffer.ML		\
-  General/file.ML General/graph.ML General/heap.ML General/integer.ML	\
-  General/lazy.ML General/markup.ML General/name_space.ML		\
-  General/ord_list.ML General/output.ML General/path.ML			\
-  General/position.ML General/pretty.ML General/print_mode.ML		\
-  General/properties.ML General/queue.ML General/scan.ML		\
-  General/secure.ML General/seq.ML General/source.ML General/stack.ML	\
-  General/symbol.ML General/symbol_pos.ML General/table.ML		\
-  General/url.ML General/xml.ML General/yxml.ML Isar/ROOT.ML		\
-  Isar/antiquote.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML	\
-  Isar/calculation.ML Isar/class.ML Isar/code.ML Isar/code_unit.ML	\
-  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
-  Isar/expression.ML							\
-  Isar/find_theorems.ML Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML	\
-  Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML		\
-  Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML	\
-  Isar/new_locale.ML    \
+  Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
+  Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
+  General/alist.ML General/balanced_tree.ML General/basics.ML		\
+  General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
+  General/integer.ML General/lazy.ML General/markup.ML			\
+  General/name_space.ML General/ord_list.ML General/output.ML		\
+  General/path.ML General/position.ML General/pretty.ML			\
+  General/print_mode.ML General/properties.ML General/queue.ML		\
+  General/scan.ML General/secure.ML General/seq.ML General/source.ML	\
+  General/stack.ML General/symbol.ML General/symbol_pos.ML		\
+  General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
+  Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
+  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/code.ML	\
+  Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML		\
+  Isar/element.ML Isar/expression.ML Isar/find_theorems.ML		\
+  Isar/instance.ML Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
+  Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
+  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/new_locale.ML	\
   Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
   Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
   Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
@@ -76,17 +74,16 @@
   Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML	\
   Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML		\
   Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML	\
-  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML 	\
-  Tools/isabelle_process.ML Tools/named_thms.ML		\
-  Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
-  conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
-  defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
-  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
-  morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML	\
-  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML		\
-  simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML	\
-  term_subst.ML theory.ML thm.ML type.ML type_infer.ML unify.ML		\
-  variable.ML ../Tools/value.ML ../Tools/quickcheck.ML
+  Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML			\
+  Tools/isabelle_process.ML Tools/named_thms.ML Tools/xml_syntax.ML	\
+  assumption.ML axclass.ML codegen.ML config.ML conjunction.ML		\
+  consts.ML context.ML context_position.ML conv.ML defs.ML display.ML	\
+  drule.ML envir.ML facts.ML goal.ML interpretation.ML library.ML	\
+  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
+  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML	\
+  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML	\
+  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML	\
+  type_infer.ML unify.ML variable.ML ../Tools/quickcheck.ML
 	@./mk
 
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Isar/proof.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/Isar/proof.ML
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 The Isar/VM proof language interpreter: maintains a structured flow of
@@ -826,7 +825,7 @@
     |> null props ? (refine (Method.Basic (Method.assumption, Position.none)) #> Seq.hd)
   end;
 
-fun generic_qed state =
+fun generic_qed after_ctxt state =
   let
     val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state;
     val outer_state = state |> close_block;
@@ -845,7 +844,7 @@
     fun after_global' x y = Position.setmp_thread_data pos (fn () => after_global x y) ();
   in
     outer_state
-    |> map_context (ProofContext.auto_bind_facts props)
+    |> map_context (after_ctxt props)
     |> pair ((after_local', after_global'), results)
   end;
 
@@ -872,7 +871,8 @@
 
 fun local_qed txt =
   end_proof false txt #>
-  Seq.maps (generic_qed #-> (fn ((after_qed, _), results) => after_qed results));
+  Seq.maps (generic_qed ProofContext.auto_bind_facts #->
+    (fn ((after_qed, _), results) => after_qed results));
 
 
 (* global goals *)
@@ -892,7 +892,7 @@
 
 fun global_qeds txt =
   end_proof true txt
-  #> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) =>
+  #> Seq.map (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
     after_qed results (context_of state)))
   |> Seq.DETERM;   (*backtracking may destroy theory!*)
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Isar/theory_target.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,6 +1,4 @@
 (*  Title:      Pure/Isar/theory_target.ML
-    ID:         $Id$
-    ID:         $Id$
     Author:     Makarius
 
 Common theory/locale/class/instantiation/overloading targets.
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Isar/toplevel.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -718,7 +718,7 @@
 
         val future_proof = Proof.future_proof
           (fn prf =>
-            Future.fork_background (fn () =>
+            Future.fork_pri 1 (fn () =>
               let val (states, State (result_node, _)) =
                 (case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev)
                   => State (SOME (Proof (ProofNode.init prf, (finish, orig_gthy)), exit), prev))
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/ROOT.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -87,8 +87,6 @@
 
 cd "Tools"; use "ROOT.ML"; cd "..";
 
-use "../Tools/value.ML";
-use "../Tools/quickcheck.ML";
 use "codegen.ML";
 
 (*configuration for Proof General*)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Thy/thy_info.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -315,7 +315,13 @@
 datatype task = Task of (unit -> unit) | Finished | Running;
 fun task_finished Finished = true | task_finished _ = false;
 
-fun future_schedule task_graph =
+local
+
+fun schedule_seq tasks =
+  Graph.topological_order tasks
+  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
+
+fun schedule_futures task_graph =
   let
     val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
       (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
@@ -339,45 +345,14 @@
     val proof_results = PureThy.join_proofs (map_filter (try get_theory o #1) tasks);
   in ignore (Exn.release_all (thy_results @ proof_results)) end;
 
-local
-
-fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m))
-  | max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) =
-      if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task'
-  | max_task _ task' = task';
-
-fun next_task G =
-  let
-    val tasks = Graph.minimals G |> map (fn name =>
-      (name, (Graph.get_node G name, length (Graph.imm_succs G name))));
-    val finished = filter (task_finished o fst o snd) tasks;
-  in
-    if not (null finished) then next_task (Graph.del_nodes (map fst finished) G)
-    else if null tasks then (Schedule.Terminate, G)
-    else
-      (case fold max_task tasks NONE of
-        NONE => (Schedule.Wait, G)
-      | SOME (name, (body, _)) =>
-         (Schedule.Task {body = PrintMode.closure body,
-           cont = Graph.del_nodes [name], fail = K Graph.empty},
-          Graph.map_node name (K Running) G))
-  end;
-
-fun schedule_seq tasks =
-  Graph.topological_order tasks
-  |> List.app (fn name => (case Graph.get_node tasks name of Task body => body () | _ => ()));
-
 in
 
 fun schedule_tasks tasks n =
-  let val m = Multithreading.max_threads_value () in
-    if m <= 1 then schedule_seq tasks
-    else if Multithreading.self_critical () then
+  if not (Multithreading.enabled ()) then schedule_seq tasks
+  else if Multithreading.self_critical () then
      (warning (loader_msg "no multithreading within critical section" []);
       schedule_seq tasks)
-    else if Future.enabled () then future_schedule tasks
-    else ignore (Exn.release_all (map Exn.Exn (Schedule.schedule (Int.min (m, n)) next_task tasks)))
-  end;
+  else schedule_futures tasks;
 
 end;
 
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/Tools/ROOT.ML
--- a/src/Pure/Tools/ROOT.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/Tools/ROOT.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -11,3 +11,6 @@
 
 (*derived theory and proof elements*)
 use "invoke.ML";
+
+(*quickcheck needed here because of pg preferences*)
+use "../../Tools/quickcheck.ML"
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/codegen.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1025,8 +1025,6 @@
 
 val setup = add_codegen "default" default_codegen
   #> add_tycodegen "default" default_tycodegen
-  #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
-  #> Quickcheck.add_generator ("SML", test_term)
   #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
        (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)))
   #> add_preprocessor unfold_preprocessor;
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/context.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -21,11 +21,10 @@
   val ancestors_of: theory -> theory list
   val theory_name: theory -> string
   val is_stale: theory -> bool
-  val PureN: string
   val is_draft: theory -> bool
   val reject_draft: theory -> theory
-  val exists_name: string -> theory -> bool
-  val names_of: theory -> string list
+  val PureN: string
+  val display_names: theory -> string list
   val pretty_thy: theory -> Pretty.T
   val string_of_thy: theory -> string
   val pprint_thy: theory -> pprint_args -> unit
@@ -144,17 +143,18 @@
 datatype theory =
   Theory of
    (*identity*)
-   {self: theory ref option,            (*dynamic self reference -- follows theory changes*)
-    id: serial * (string * int),        (*identifier/name of this theory node*)
-    ids: (string * int) Inttab.table} * (*ancestors and checkpoints*)
+   {self: theory ref option,      (*dynamic self reference -- follows theory changes*)
+    draft: bool,                  (*draft mode -- linear destructive changes*)
+    id: serial,                   (*identifier*)
+    ids: unit Inttab.table} *     (*cumulative identifiers of non-drafts -- symbolic body content*)
    (*data*)
-   Object.T Datatab.table *
+   Object.T Datatab.table *       (*body content*)
    (*ancestry*)
-   {parents: theory list,               (*immediate predecessors*)
-    ancestors: theory list} *           (*all predecessors*)
+   {parents: theory list,         (*immediate predecessors*)
+    ancestors: theory list} *     (*all predecessors -- canonical reverse order*)
    (*history*)
-   {name: string,                       (*prospective name of finished theory*)
-    version: int};                      (*checkpoint counter*)
+   {name: string,                 (*official theory name*)
+    stage: int};                  (*checkpoint counter*)
 
 exception THEORY of string * theory list;
 
@@ -165,9 +165,9 @@
 val ancestry_of = #3 o rep_theory;
 val history_of  = #4 o rep_theory;
 
-fun make_identity self id ids = {self = self, id = id, ids = ids};
+fun make_identity self draft id ids = {self = self, draft = draft, id = id, ids = ids};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
-fun make_history name version = {name = name, version = version};
+fun make_history name stage = {name = name, stage = stage};
 
 val the_self = the o #self o identity_of;
 val parents_of = #parents o ancestry_of;
@@ -177,7 +177,7 @@
 
 (* staleness *)
 
-fun eq_id ((i: int, _), (j, _)) = (i = j);
+fun eq_id (i: int, j) = i = j;
 
 fun is_stale
     (Theory ({self = SOME (ref (Theory ({id = id', ...}, _, _, _))), id, ...}, _, _, _)) =
@@ -185,47 +185,46 @@
   | is_stale (Theory ({self = NONE, ...}, _, _, _)) = true;
 
 fun vitalize (thy as Theory ({self = SOME r, ...}, _, _, _)) = (r := thy; thy)
-  | vitalize (thy as Theory ({self = NONE, id, ids}, data, ancestry, history)) =
+  | vitalize (thy as Theory ({self = NONE, draft, id, ids}, data, ancestry, history)) =
       let
         val r = ref thy;
-        val thy' = Theory (make_identity (SOME r) id ids, data, ancestry, history);
+        val thy' = Theory (make_identity (SOME r) draft id ids, data, ancestry, history);
       in r := thy'; thy' end;
 
 
-(* names *)
-
-val PureN = "Pure";
+(* draft mode *)
 
-val draftN = "#";
-val draft_name = (draftN, ~1);
-
-fun draft_id (_, (name, _)) = (name = draftN);
-val is_draft = draft_id o #id o identity_of;
+val is_draft = #draft o identity_of;
 
 fun reject_draft thy =
   if is_draft thy then raise THEORY ("Illegal draft theory -- stable checkpoint required", [thy])
   else thy;
 
-fun exists_name name (thy as Theory ({id = (_, (a, _)), ids, ...}, _, _, _)) =
-  name = theory_name thy orelse
-  name = a orelse
-  Inttab.exists (fn (_, (b, _)) => b = name) ids;
+
+(* names *)
+
+val PureN = "Pure";
+val draftN = "#";
+val finished = ~1;
 
-fun name_of (a, ~1) = a
-  | name_of (a, i) = a ^ ":" ^ string_of_int i;
+fun display_names thy =
+  let
+    val draft = if is_draft thy then [draftN] else [];
+    val {stage, ...} = history_of thy;
+    val name =
+      if stage = finished then theory_name thy
+      else theory_name thy ^ ":" ^ string_of_int stage;
+    val ancestor_names = map theory_name (ancestors_of thy);
+    val stale = if is_stale thy then ["!"] else [];
+  in rev (stale @ draft @ [name] @ ancestor_names) end;
 
-fun names_of (Theory ({id = (_, a), ids, ...}, _, _, _)) =
-  rev (name_of a :: Inttab.fold (fn (_, (b, ~1)) => cons b | _ => I) ids []);
-
-fun pretty_thy thy =
-  Pretty.str_list "{" "}" (names_of thy @ (if is_stale thy then ["!"] else []));
-
+val pretty_thy = Pretty.str_list "{" "}" o display_names;
 val string_of_thy = Pretty.string_of o pretty_thy;
 val pprint_thy = Pretty.pprint o pretty_thy;
 
 fun pretty_abbrev_thy thy =
   let
-    val names = names_of thy;
+    val names = display_names thy;
     val n = length names;
     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   in Pretty.str_list "{" "}" abbrev end;
@@ -252,20 +251,18 @@
 val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
 
 
-(* consistency *)
+(* build ids *)
+
+fun insert_id draft id ids =
+  if draft then ids
+  else Inttab.update (id, ()) ids;
 
-fun check_insert id ids =
-  if draft_id id orelse Inttab.defined ids (#1 id) then ids
-  else if Inttab.exists (fn (_, a) => a = #2 id) ids then
-    error ("Different versions of theory component " ^ quote (name_of (#2 id)))
-  else Inttab.update id ids;
-
-fun check_merge
-    (Theory ({id = id1, ids = ids1, ...}, _, _, _))
-    (Theory ({id = id2, ids = ids2, ...}, _, _, _)) =
-  Inttab.fold check_insert ids2 ids1
-  |> check_insert id1
-  |> check_insert id2;
+fun merge_ids
+    (Theory ({draft = draft1, id = id1, ids = ids1, ...}, _, _, _))
+    (Theory ({draft = draft2, id = id2, ids = ids2, ...}, _, _, _)) =
+  Inttab.merge (K true) (ids1, ids2)
+  |> insert_id draft1 id1
+  |> insert_id draft2 id2;
 
 
 (* equality and inclusion *)
@@ -273,22 +270,35 @@
 val eq_thy = eq_id o pairself (#id o identity_of);
 
 fun proper_subthy (Theory ({id, ...}, _, _, _), Theory ({ids, ...}, _, _, _)) =
-  Inttab.defined ids (#1 id);
+  Inttab.defined ids id;
 
 fun subthy thys = eq_thy thys orelse proper_subthy thys;
 
 fun joinable (thy1, thy2) = subthy (thy1, thy2) orelse subthy (thy2, thy1);
 
 
+(* consistent ancestors *)
+
+fun extend_ancestors thy thys =
+  if member eq_thy thys thy then raise THEORY ("Duplicate theory node", thy :: thys)
+  else thy :: thys;
+
+fun extend_ancestors_of thy = extend_ancestors thy (ancestors_of thy);
+
+val merge_ancestors = merge (fn (thy1, thy2) =>
+  eq_thy (thy1, thy2) orelse
+    theory_name thy1 = theory_name thy2 andalso
+      raise THEORY ("Inconsistent theory versions", [thy1, thy2]));
+
+
 (* trivial merge *)
 
 fun merge (thy1, thy2) =
   if eq_thy (thy1, thy2) then thy1
   else if proper_subthy (thy2, thy1) then thy1
   else if proper_subthy (thy1, thy2) then thy2
-  else (check_merge thy1 thy2;
-    error (cat_lines ["Attempt to perform non-trivial merge of theories:",
-      str_of_thy thy1, str_of_thy thy2]));
+  else error (cat_lines ["Attempt to perform non-trivial merge of theories:",
+    str_of_thy thy1, str_of_thy thy2]);
 
 fun merge_refs (ref1, ref2) =
   if ref1 = ref2 then ref1
@@ -300,41 +310,38 @@
 
 (* primitives *)
 
-fun create_thy name self id ids data ancestry history =
-  let
-    val {version, ...} = history;
-    val ids' = check_insert id ids;
-    val id' = (serial (), name);
-    val _ = check_insert id' ids';
-    val identity' = make_identity self id' ids';
-  in vitalize (Theory (identity', data, ancestry, history)) end;
+fun create_thy self draft ids data ancestry history =
+  let val identity = make_identity self draft (serial ()) ids;
+  in vitalize (Theory (identity, data, ancestry, history)) end;
 
-fun change_thy name f thy =
+fun change_thy draft' f thy =
   let
-    val Theory ({self, id, ids}, data, ancestry, history) = thy;
+    val Theory ({self, draft, id, ids}, data, ancestry, history) = thy;
     val (self', data', ancestry') =
-      if is_draft thy then (self, data, ancestry)    (*destructive change!*)
-      else if #version history > 0
+      if draft then (self, data, ancestry)    (*destructive change!*)
+      else if #stage history > 0
       then (NONE, copy_data data, ancestry)
-      else (NONE, extend_data data, make_ancestry [thy] (thy :: #ancestors ancestry));
+      else (NONE, extend_data data, make_ancestry [thy] (extend_ancestors_of thy));
+    val ids' = insert_id draft id ids;
     val data'' = f data';
     val thy' = NAMED_CRITICAL "theory" (fn () =>
-      (check_thy thy; create_thy name self' id ids data'' ancestry' history));
+      (check_thy thy; create_thy self' draft' ids' data'' ancestry' history));
   in thy' end;
 
-fun name_thy name = change_thy name I;
-val modify_thy = change_thy draft_name;
-val extend_thy = modify_thy I;
+val name_thy = change_thy false I;
+val extend_thy = change_thy true I;
+val modify_thy = change_thy true;
 
 fun copy_thy thy =
   let
-    val Theory ({id, ids, ...}, data, ancestry, history) = thy;
+    val Theory ({draft, id, ids, ...}, data, ancestry, history) = thy;
+    val ids' = insert_id draft id ids;
     val data' = copy_data data;
     val thy' = NAMED_CRITICAL "theory" (fn () =>
-      (check_thy thy; create_thy draft_name NONE id ids data' ancestry history));
+      (check_thy thy; create_thy NONE true ids' data' ancestry history));
   in thy' end;
 
-val pre_pure_thy = create_thy draft_name NONE (serial (), draft_name) Inttab.empty
+val pre_pure_thy = create_thy NONE true Inttab.empty
   Datatab.empty (make_ancestry [] []) (make_history PureN 0);
 
 
@@ -342,56 +349,56 @@
 
 fun merge_thys pp (thy1, thy2) =
   let
-    val ids = check_merge thy1 thy2;
+    val ids = merge_ids thy1 thy2;
     val data = merge_data (pp thy1) (data_of thy1, data_of thy2);
     val ancestry = make_ancestry [] [];
     val history = make_history "" 0;
     val thy' = NAMED_CRITICAL "theory" (fn () =>
-     (check_thy thy1; check_thy thy2;
-      create_thy draft_name NONE (serial (), draft_name) ids data ancestry history));
+     (check_thy thy1; check_thy thy2; create_thy NONE true ids data ancestry history));
   in thy' end;
 
 fun maximal_thys thys =
   thys |> filter_out (fn thy => exists (fn thy' => proper_subthy (thy, thy')) thys);
 
 fun begin_thy pp name imports =
-  if name = draftN then error ("Illegal theory name: " ^ quote draftN)
+  if name = "" orelse name = draftN then error ("Bad theory name: " ^ quote name)
   else
     let
       val parents = maximal_thys (distinct eq_thy imports);
-      val ancestors = distinct eq_thy (parents @ maps ancestors_of parents);
-      val Theory ({id, ids, ...}, data, _, _) =
+      val ancestors =
+        Library.foldl merge_ancestors ([], map ancestors_of parents)
+        |> fold extend_ancestors parents;
+
+      val Theory ({ids, ...}, data, _, _) =
         (case parents of
           [] => error "No parent theories"
         | [thy] => extend_thy thy
         | thy :: thys => Library.foldl (merge_thys pp) (thy, thys));
+
       val ancestry = make_ancestry parents ancestors;
       val history = make_history name 0;
       val thy' = NAMED_CRITICAL "theory" (fn () =>
-        (map check_thy imports; create_thy draft_name NONE id ids data ancestry history));
+        (map check_thy imports; create_thy NONE true ids data ancestry history));
     in thy' end;
 
 
-(* persistent checkpoints *)
+(* history stages *)
+
+fun history_stage f thy =
+  let
+    val {name, stage} = history_of thy;
+    val _ = stage = finished andalso raise THEORY ("Theory already finished", [thy]);
+    val history' = make_history name (f stage);
+    val thy' as Theory (identity', data', ancestry', _) = name_thy thy;
+    val thy'' = NAMED_CRITICAL "theory" (fn () =>
+      (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
+  in thy'' end;
 
 fun checkpoint_thy thy =
-  if not (is_draft thy) then thy
-  else
-    let
-      val {name, version} = history_of thy;
-      val thy' as Theory (identity', data', ancestry', _) = name_thy (name, version) thy;
-      val history' = make_history name (version + 1);
-      val thy'' = NAMED_CRITICAL "theory" (fn () =>
-        (check_thy thy'; vitalize (Theory (identity', data', ancestry', history'))));
-    in thy'' end;
+  if is_draft thy then history_stage (fn stage => stage + 1) thy
+  else thy;
 
-fun finish_thy thy = NAMED_CRITICAL "theory" (fn () =>
-  let
-    val name = theory_name thy;
-    val Theory (identity', data', ancestry', _) = name_thy (name, ~1) thy;
-    val history' = make_history name 0;
-    val thy' = vitalize (Theory (identity', data', ancestry', history'));
-  in thy' end);
+val finish_thy = history_stage (fn _ => finished);
 
 
 (* theory data *)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/display.ML
--- a/src/Pure/display.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/display.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -213,7 +213,7 @@
       ||> List.partition (Defs.plain_args o #2 o #1);
     val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
   in
-    [Pretty.strs ("names:" :: Context.names_of thy)] @
+    [Pretty.strs ("names:" :: Context.display_names thy)] @
     [Pretty.strs ["name prefix:", NameSpace.path_of naming],
       Pretty.big_list "classes:" (map pretty_classrel clsses),
       pretty_default default,
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/goal.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -179,7 +179,7 @@
     val res =
       if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (Future.enabled ())
       then result ()
-      else future_result ctxt' (Future.fork_background result) (Thm.term_of stmt);
+      else future_result ctxt' (Future.fork_pri 1 result) (Thm.term_of stmt);
   in
     Conjunction.elim_balanced (length props) res
     |> map (Assumption.export false ctxt' ctxt)
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/old_goals.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -127,7 +127,7 @@
 
 (*Generates the list of new theories when the proof state's theory changes*)
 fun thy_error (thy,thy') =
-  let val names = Context.names_of thy' \\ Context.names_of thy
+  let val names = Context.display_names thy' \\ Context.display_names thy
   in  case names of
         [name] => "\nNew theory: " ^ name
       | _       => "\nNew theories: " ^ space_implode ", " names
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/pure_setup.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      Pure/pure_setup.ML
-    ID:         $Id$
     Author:     Makarius
 
 Pure theory and ML toplevel setup.
@@ -28,8 +27,8 @@
 
 (* ML toplevel pretty printing *)
 
-install_pp (make_pp ["TaskQueue", "task"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_task));
-install_pp (make_pp ["TaskQueue", "group"] (Pretty.pprint o Pretty.str o TaskQueue.str_of_group));
+install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
+install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
 install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
diff -r 685c9e05a6ab -r fd8bb7527f7b src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Dec 16 09:44:59 2008 -0800
+++ b/src/Pure/theory.ML	Tue Dec 16 21:18:53 2008 -0800
@@ -68,7 +68,7 @@
 val copy = Context.copy_thy;
 
 fun requires thy name what =
-  if Context.exists_name name thy then ()
+  if exists (fn thy' => Context.theory_name thy' = name) (thy :: ancestors_of thy) then ()
   else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what);