merged; closure-solver
authorLukas Stevens <mail@lukas-stevens.de>
Thu, 23 Sep 2021 11:26:15 +0200
branchclosure-solver
changeset 74715 f7a8c4470e32
parent 74683 38b28a04a4ef (current diff)
parent 74713 6203d4154426 (diff)
child 74716 a744e9a22655
merged;
src/HOL/Transitive_Closure.thy
--- a/Admin/components/components.sha1	Tue Sep 21 14:54:53 2021 +0200
+++ b/Admin/components/components.sha1	Thu Sep 23 11:26:15 2021 +0200
@@ -136,6 +136,7 @@
 4554679cc8ea31e539655810a14d14216b383d0e  isabelle_setup-20210724-2.tar.gz
 127a75ae33e97480d352087fcb9b47a632d77169  isabelle_setup-20210724.tar.gz
 309909ec6d43ae460338e9af54c1b2a48adcb1ec  isabelle_setup-20210726.tar.gz
+a14ce46c62c64c3413f3cc9239242e33570d0f3d  isabelle_setup-20210922.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544  jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56  jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39  jdk-11.0.2+9.tar.gz
@@ -147,6 +148,7 @@
 71d19df63816e9be1c4c5eb44aea7a44cfadb319  jdk-11.tar.gz
 72455a2fdb6cced9cd563f4d5d6134f7a6c34913  jdk-15.0.1+9.tar.gz
 e8ae300e61b0b121018456d50010b555bc96ce10  jdk-15.0.2+7.tar.gz
+a426a32ad34014953c0f7d4cc6f44199572e1c38  jdk-17+35.tar.gz
 8d83e433c1419e0c0cc5fd1762903d11b4a5752c  jdk-6u31.tar.gz
 38d2d2a91c66714c18430e136e7e5191af3996e6  jdk-7u11.tar.gz
 d765bc4ad2f34d494429b2a8c1563c49db224944  jdk-7u13.tar.gz
--- a/Admin/components/main	Tue Sep 21 14:54:53 2021 +0200
+++ b/Admin/components/main	Thu Sep 23 11:26:15 2021 +0200
@@ -8,14 +8,13 @@
 flatlaf-1.2
 idea-icons-20210508
 isabelle_fonts-20210322
-isabelle_setup-20210726
-jdk-15.0.2+7
+isabelle_setup-20210922
+jdk-17+35
 jedit-20210802
 jfreechart-1.5.1
 jortho-1.0-2
 kodkodi-1.5.6-1
 nunchaku-0.5
-old_vampire-4.2.2
 opam-2.0.7
 polyml-5.8.2
 postgresql-42.2.18
--- a/NEWS	Tue Sep 21 14:54:53 2021 +0200
+++ b/NEWS	Thu Sep 23 11:26:15 2021 +0200
@@ -9,12 +9,18 @@
 
 *** General ***
 
+* Commands 'syntax' and 'no_syntax' now work in a local theory context,
+but there is no proper way to refer to local entities --- in contrast to
+'notation' and 'no_notation'. Local syntax works well with 'bundle',
+e.g. see "lattice_syntax" vs. "no_lattice_syntax" in theory Main of
+Isabelle/HOL.
+
 * Configuration option "show_results" controls output of final results
 in commands like 'definition' or 'theorem'. Output is normally enabled
 in interactive mode, but it could occasionally cause unnecessary
 slowdown. It can be disabled like this:
 
-  context notes [[show_results = true]]
+  context notes [[show_results = false]]
   begin
     definition "test = True"
     theorem test by (simp add: test_def)
@@ -128,6 +134,11 @@
 
 *** HOL ***
 
+* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
+"lattice_syntax": it can be used in a local context via 'include' or in
+a global theory via 'unbundle'. The opposite declarations are bundled as
+"no_lattice_syntax". Minor INCOMPATIBILITY.
+
 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,
 use explict expression instead. Minor INCOMPATIBILITY.
 
@@ -251,6 +262,10 @@
 * ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
 corresponding ML values, notably as arguments for Thm.instantiate etc.
 
+* ML antiquotations \<^make_judgment> and \<^dest_judgment> refer to
+corresponding functions for the object-logic of the ML compilation
+context. This supersedes older mk_Trueprop / dest_Trueprop operations.
+
 * ML antiquotations for type constructors and term constants:
 
     \<^Type>\<open>c\<close>
--- a/etc/symbols	Tue Sep 21 14:54:53 2021 +0200
+++ b/etc/symbols	Thu Sep 23 11:26:15 2021 +0200
@@ -456,6 +456,8 @@
 \<^ctyp>                argument: cartouche
 \<^keyword>             argument: cartouche
 \<^locale>              argument: cartouche
+\<^make_judgment>
+\<^dest_judgment>
 \<^make_string>
 \<^method>              argument: cartouche
 \<^named_theorems>      argument: cartouche
--- a/lib/texinputs/isabellesym.sty	Tue Sep 21 14:54:53 2021 +0200
+++ b/lib/texinputs/isabellesym.sty	Thu Sep 23 11:26:15 2021 +0200
@@ -446,6 +446,8 @@
 \newcommand{\isactrlkeyword}{\isakeywordcontrol{keyword}}
 \newcommand{\isactrllatex}{\isakeywordcontrol{latex}}
 \newcommand{\isactrllocale}{\isakeywordcontrol{locale}}
+\newcommand{\isactrlmakeUNDERSCOREjudgment}{\isakeywordcontrol{make{\isacharunderscore}judgment}}
+\newcommand{\isactrldestUNDERSCOREjudgment}{\isakeywordcontrol{dest{\isacharunderscore}judgment}}
 \newcommand{\isactrlmakeUNDERSCOREstring}{\isakeywordcontrol{make{\isacharunderscore}string}}
 \newcommand{\isactrlmasterUNDERSCOREdir}{\isakeywordcontrol{master{\isacharunderscore}dir}}
 \newcommand{\isactrlmethod}{\isakeywordcontrol{method}}
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -1077,8 +1077,8 @@
 text \<open>
   \begin{tabular}{rcll}
     @{command_def "nonterminal"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def "syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
-    @{command_def "no_syntax"} & : & \<open>theory \<rightarrow> theory\<close> \\
+    @{command_def "syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+    @{command_def "no_syntax"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     @{command_def "translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{command_def "no_translations"} & : & \<open>theory \<rightarrow> theory\<close> \\
     @{attribute_def syntax_ast_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
--- a/src/Doc/Main/Main_Doc.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -89,7 +89,7 @@
 
 \subsubsection*{Syntax}
 
-Available by loading theory \<open>Lattice_Syntax\<close> in directory \<open>Library\<close>.
+Available via \<^theory_text>\<open>unbundle lattice_syntax\<close>.
 
 \begin{supertabular}{@ {} l @ {\quad$\equiv$\quad} l @ {}}
 @{text[source]"x \<sqsubseteq> y"} & \<^term>\<open>x \<le> y\<close>\\
--- a/src/Doc/Sledgehammer/document/root.tex	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Thu Sep 23 11:26:15 2021 +0200
@@ -159,9 +159,7 @@
 \begin{enum}
 \item[\labelitemi] If you installed an official Isabelle package, it should
 already include properly set up executables for CVC4, E, SPASS, Vampire, veriT,
-and Z3, ready to use. To use Vampire, you must confirm that you are a
-noncommercial user, as indicated by the message that is displayed when
-Sledgehammer is invoked the first time.
+and Z3, ready to use.
 
 \item[\labelitemi] Alternatively, you can download the Isabelle-aware CVC4, E,
 SPASS, Vampire, veriT, and Z3 binary packages from \download. Extract the
--- a/src/Doc/Typeclass_Hierarchy/Setup.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Doc/Typeclass_Hierarchy/Setup.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -1,7 +1,9 @@
 theory Setup
-imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
+imports Complex_Main "HOL-Library.Multiset"
 begin
 
+unbundle lattice_syntax
+
 ML_file \<open>../antiquote_setup.ML\<close>
 ML_file \<open>../more_antiquote.ML\<close>
 
--- a/src/FOL/IFOL.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/FOL/IFOL.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -527,7 +527,7 @@
 structure Hypsubst = Hypsubst
 (
   val dest_eq = FOLogic.dest_eq
-  val dest_Trueprop = FOLogic.dest_Trueprop
+  val dest_Trueprop = \<^dest_judgment>
   val dest_imp = FOLogic.dest_imp
   val eq_reflection = @{thm eq_reflection}
   val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
--- a/src/FOL/fologic.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/FOL/fologic.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -6,8 +6,6 @@
 
 signature FOLOGIC =
 sig
-  val mk_Trueprop: term -> term
-  val dest_Trueprop: term -> term
   val mk_conj: term * term -> term
   val mk_disj: term * term -> term
   val mk_imp: term * term -> term
@@ -24,10 +22,6 @@
 structure FOLogic: FOLOGIC =
 struct
 
-fun mk_Trueprop P = \<^Const>\<open>Trueprop for P\<close>;
-
-val dest_Trueprop = \<^Const_fn>\<open>Trueprop for P => P\<close>;
-
 fun mk_conj (t1, t2) = \<^Const>\<open>conj for t1 t2\<close>
 and mk_disj (t1, t2) = \<^Const>\<open>disj for t1 t2\<close>
 and mk_imp (t1, t2) = \<^Const>\<open>imp for t1 t2\<close>
--- a/src/HOL/Complete_Lattices.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Complete_Lattices.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -15,10 +15,10 @@
 subsection \<open>Syntactic infimum and supremum operations\<close>
 
 class Inf =
-  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter>")
+  fixes Inf :: "'a set \<Rightarrow> 'a"  ("\<Sqinter> _" [900] 900)
 
 class Sup =
-  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion>")
+  fixes Sup :: "'a set \<Rightarrow> 'a"  ("\<Squnion> _" [900] 900)
 
 syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
--- a/src/HOL/Examples/Knaster_Tarski.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Examples/Knaster_Tarski.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -7,9 +7,11 @@
 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>
 
 theory Knaster_Tarski
-  imports Main "HOL-Library.Lattice_Syntax"
+  imports Main
 begin
 
+unbundle lattice_syntax
+
 
 subsection \<open>Prose version\<close>
 
--- a/src/HOL/Library/Combine_PER.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Library/Combine_PER.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -3,9 +3,11 @@
 section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
 
 theory Combine_PER
-  imports Main Lattice_Syntax
+  imports Main
 begin
 
+unbundle lattice_syntax
+
 definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"
 
--- a/src/HOL/Library/Complete_Partial_Order2.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Library/Complete_Partial_Order2.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -5,9 +5,11 @@
 section \<open>Formalisation of chain-complete partial orders, continuity and admissibility\<close>
 
 theory Complete_Partial_Order2 imports 
-  Main Lattice_Syntax
+  Main
 begin
 
+unbundle lattice_syntax
+
 lemma chain_transfer [transfer_rule]:
   includes lifting_syntax
   shows "((A ===> A ===> (=)) ===> rel_set A ===> (=)) Complete_Partial_Order.chain Complete_Partial_Order.chain"
--- a/src/HOL/Library/Lattice_Syntax.thy	Tue Sep 21 14:54:53 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,23 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-section \<open>Pretty syntax for lattice operations\<close>
-
-theory Lattice_Syntax
-imports Main
-begin
-
-notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter> _" [900] 900) and
-  Sup  ("\<Squnion> _" [900] 900)
-
-syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
-end
--- a/src/HOL/Library/Library.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Library/Library.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -46,7 +46,6 @@
   IArray
   Landau_Symbols
   Lattice_Algebras
-  Lattice_Syntax
   Lattice_Constructions
   Linear_Temporal_Logic_on_Streams
   ListVector
--- a/src/HOL/Library/Option_ord.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Library/Option_ord.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -8,20 +8,7 @@
 imports Main
 begin
 
-notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter> _" [900] 900) and
-  Sup  ("\<Squnion> _" [900] 900)
-
-syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
-
+unbundle lattice_syntax
 
 instantiation option :: (preorder) preorder
 begin
@@ -462,19 +449,6 @@
 
 instance option :: (complete_linorder) complete_linorder ..
 
-
-no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf  (infixl "\<sqinter>" 70) and
-  sup  (infixl "\<squnion>" 65) and
-  Inf  ("\<Sqinter> _" [900] 900) and
-  Sup  ("\<Squnion> _" [900] 900)
-
-no_syntax
-  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
-  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
-  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
-  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+unbundle no_lattice_syntax
 
 end
--- a/src/HOL/Library/code_lazy.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Library/code_lazy.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -91,7 +91,7 @@
     val lthy' = (snd o Local_Theory.begin_nested) lthy
     val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
       ((Thm.def_binding (Binding.name name), []), def) lthy'
-    val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
+    val lthy' = Local_Theory.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
     val lthy = Local_Theory.end_nested lthy'
     val def_thm = singleton (Proof_Context.export lthy' lthy) thm
   in
--- a/src/HOL/Main.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Main.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -19,7 +19,7 @@
     GCD
 begin
 
-text \<open>Namespace cleanup\<close>
+subsection \<open>Namespace cleanup\<close>
 
 hide_const (open)
   czero cinfinite cfinite csum cone ctwo Csum cprod cexp image2 image2p vimage2p Gr Grp collect
@@ -29,15 +29,9 @@
 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
 
 
-text \<open>Syntax cleanup\<close>
+subsection \<open>Syntax cleanup\<close>
 
 no_notation
-  bot ("\<bottom>") and
-  top ("\<top>") and
-  inf (infixl "\<sqinter>" 70) and
-  sup (infixl "\<squnion>" 65) and
-  Inf ("\<Sqinter>") and
-  Sup ("\<Squnion>") and
   ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
   ordLess2 (infix "<o" 50) and
@@ -48,7 +42,9 @@
   BNF_Cardinal_Arithmetic.cexp (infixr "^c" 90) and
   BNF_Def.convol ("\<langle>(_,/ _)\<rangle>")
 
-bundle cardinal_syntax begin
+bundle cardinal_syntax
+begin
+
 notation
   ordLeq2 (infix "<=o" 50) and
   ordLeq3 (infix "\<le>o" 50) and
@@ -63,8 +59,42 @@
 alias czero = BNF_Cardinal_Arithmetic.czero
 alias cone = BNF_Cardinal_Arithmetic.cone
 alias ctwo = BNF_Cardinal_Arithmetic.ctwo
+
 end
 
+
+subsection \<open>Lattice syntax\<close>
+
+bundle lattice_syntax
+begin
+
+notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  Inf  ("\<Sqinter> _" [900] 900) and
+  Sup  ("\<Squnion> _" [900] 900)
+
+syntax
+  "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
+  "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
+  "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
+  "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+
+end
+
+bundle no_lattice_syntax
+begin
+
+no_notation
+  bot ("\<bottom>") and
+  top ("\<top>") and
+  inf  (infixl "\<sqinter>" 70) and
+  sup  (infixl "\<squnion>" 65) and
+  Inf  ("\<Sqinter> _" [900] 900) and
+  Sup  ("\<Squnion> _" [900] 900)
+
 no_syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
@@ -72,3 +102,7 @@
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 end
+
+unbundle no_lattice_syntax
+
+end
--- a/src/HOL/Tools/Meson/meson.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Meson/meson.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -105,7 +105,7 @@
     \<^try>\<open>
       let val thy = Proof_Context.theory_of ctxt
           val tmA = Thm.concl_of thA
-          val Const(\<^const_name>\<open>Pure.imp\<close>,_) $ tmB $ _ = Thm.prop_of thB
+          val \<^Const_>\<open>Pure.imp for tmB _\<close> = Thm.prop_of thB
           val tenv =
             Pattern.first_order_match thy (tmB, tmA)
                                           (Vartab.empty, Vartab.empty) |> snd
@@ -136,8 +136,8 @@
       | some_eq _ _ = false
     fun add_names quant (Const (quant_s, _) $ Abs (s, _, t')) =
         add_names quant t' #> some_eq quant (quant_of quant_s) ? cons s
-      | add_names quant (\<^const>\<open>Not\<close> $ t) = add_names (flip_quant quant) t
-      | add_names quant (\<^const>\<open>implies\<close> $ t1 $ t2) =
+      | add_names quant \<^Const_>\<open>Not for t\<close> = add_names (flip_quant quant) t
+      | add_names quant \<^Const_>\<open>implies for t1 t2\<close> =
         add_names (flip_quant quant) t1 #> add_names quant t2
       | add_names quant (t1 $ t2) = fold (add_names quant) [t1, t2]
       | add_names _ _ = I
@@ -174,7 +174,7 @@
    workaround is to instantiate "?P := (%c. ... c ... c ... c ...)" manually. *)
 fun quant_resolve_tac ctxt th i st =
   case (Thm.concl_of st, Thm.prop_of th) of
-    (\<^const>\<open>Trueprop\<close> $ (Var _ $ (c as Free _)), \<^const>\<open>Trueprop\<close> $ _) =>
+    (\<^Const_>\<open>Trueprop for \<open>Var _ $ (c as Free _)\<close>\<close>, \<^Const_>\<open>Trueprop for _\<close>) =>
     let
       val cc = Thm.cterm_of ctxt c
       val ct = Thm.dest_arg (Thm.cprop_of th)
@@ -202,21 +202,21 @@
 (*Are any of the logical connectives in "bs" present in the term?*)
 fun has_conns bs =
   let fun has (Const _) = false
-        | has (Const(\<^const_name>\<open>Trueprop\<close>,_) $ p) = has p
-        | has (Const(\<^const_name>\<open>Not\<close>,_) $ p) = has p
-        | has (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ p $ q) = member (op =) bs \<^const_name>\<open>HOL.disj\<close> orelse has p orelse has q
-        | has (Const(\<^const_name>\<open>HOL.conj\<close>,_) $ p $ q) = member (op =) bs \<^const_name>\<open>HOL.conj\<close> orelse has p orelse has q
-        | has (Const(\<^const_name>\<open>All\<close>,_) $ Abs(_,_,p)) = member (op =) bs \<^const_name>\<open>All\<close> orelse has p
-        | has (Const(\<^const_name>\<open>Ex\<close>,_) $ Abs(_,_,p)) = member (op =) bs \<^const_name>\<open>Ex\<close> orelse has p
+        | has \<^Const_>\<open>Trueprop for p\<close> = has p
+        | has \<^Const_>\<open>Not for p\<close> = has p
+        | has \<^Const_>\<open>disj for p q\<close> = member (op =) bs \<^const_name>\<open>disj\<close> orelse has p orelse has q
+        | has \<^Const_>\<open>conj for p q\<close> = member (op =) bs \<^const_name>\<open>conj\<close> orelse has p orelse has q
+        | has \<^Const_>\<open>All _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>All\<close> orelse has p
+        | has \<^Const_>\<open>Ex _ for \<open>Abs(_,_,p)\<close>\<close> = member (op =) bs \<^const_name>\<open>Ex\<close> orelse has p
         | has _ = false
   in  has  end;
 
 
 (**** Clause handling ****)
 
-fun literals (Const(\<^const_name>\<open>Trueprop\<close>,_) $ P) = literals P
-  | literals (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ P $ Q) = literals P @ literals Q
-  | literals (Const(\<^const_name>\<open>Not\<close>,_) $ P) = [(false,P)]
+fun literals \<^Const_>\<open>Trueprop for P\<close> = literals P
+  | literals \<^Const_>\<open>disj for P Q\<close> = literals P @ literals Q
+  | literals \<^Const_>\<open>Not for P\<close> = [(false,P)]
   | literals P = [(true,P)];
 
 (*number of literals in a term*)
@@ -225,16 +225,16 @@
 
 (*** Tautology Checking ***)
 
-fun signed_lits_aux (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ P $ Q) (poslits, neglits) =
+fun signed_lits_aux \<^Const_>\<open>disj for P Q\<close> (poslits, neglits) =
       signed_lits_aux Q (signed_lits_aux P (poslits, neglits))
-  | signed_lits_aux (Const(\<^const_name>\<open>Not\<close>,_) $ P) (poslits, neglits) = (poslits, P::neglits)
+  | signed_lits_aux \<^Const_>\<open>Not for P\<close> (poslits, neglits) = (poslits, P::neglits)
   | signed_lits_aux P (poslits, neglits) = (P::poslits, neglits);
 
 fun signed_lits th = signed_lits_aux (HOLogic.dest_Trueprop (Thm.concl_of th)) ([],[]);
 
 (*Literals like X=X are tautologous*)
-fun taut_poslit (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ t $ u) = t aconv u
-  | taut_poslit (Const(\<^const_name>\<open>True\<close>,_)) = true
+fun taut_poslit \<^Const_>\<open>HOL.eq _ for t u\<close> = t aconv u
+  | taut_poslit \<^Const_>\<open>True\<close> = true
   | taut_poslit _ = false;
 
 fun is_taut th =
@@ -261,18 +261,17 @@
 fun refl_clause_aux 0 th = th
   | refl_clause_aux n th =
        case HOLogic.dest_Trueprop (Thm.concl_of th) of
-          (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) $ _) =>
+          \<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close> =>
             refl_clause_aux n (th RS disj_assoc)    (*isolate an atom as first disjunct*)
-        | (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const(\<^const_name>\<open>Not\<close>,_) $ (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ t $ u)) $ _) =>
+        | \<^Const_>\<open>disj for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for t u\<close>\<close>\<close>\<close> _\<close> =>
             if eliminable(t,u)
             then refl_clause_aux (n-1) (th RS not_refl_disj_D)  (*Var inequation: delete*)
             else refl_clause_aux (n-1) (th RS disj_comm)  (*not between Vars: ignore*)
-        | (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) => refl_clause_aux n (th RS disj_comm)
+        | \<^Const>\<open>disj for _ _\<close> => refl_clause_aux n (th RS disj_comm)
         | _ => (*not a disjunction*) th;
 
-fun notequal_lits_count (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ P $ Q) =
-      notequal_lits_count P + notequal_lits_count Q
-  | notequal_lits_count (Const(\<^const_name>\<open>Not\<close>,_) $ (Const(\<^const_name>\<open>HOL.eq\<close>,_) $ _ $ _)) = 1
+fun notequal_lits_count \<^Const_>\<open>disj for P Q\<close> = notequal_lits_count P + notequal_lits_count Q
+  | notequal_lits_count \<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq _ for _ _\<close>\<close>\<close> = 1
   | notequal_lits_count _ = 0;
 
 (*Simplify a clause by applying reflexivity to its negated equality literals*)
@@ -317,26 +316,26 @@
   fun prod x y = if x < bound andalso y < bound then x*y else bound
   
   (*Estimate the number of clauses in order to detect infeasible theorems*)
-  fun signed_nclauses b (Const(\<^const_name>\<open>Trueprop\<close>,_) $ t) = signed_nclauses b t
-    | signed_nclauses b (Const(\<^const_name>\<open>Not\<close>,_) $ t) = signed_nclauses (not b) t
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.conj\<close>,_) $ t $ u) =
+  fun signed_nclauses b \<^Const_>\<open>Trueprop for t\<close> = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>Not for t\<close> = signed_nclauses (not b) t
+    | signed_nclauses b \<^Const_>\<open>conj for t u\<close> =
         if b then sum (signed_nclauses b t) (signed_nclauses b u)
              else prod (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.disj\<close>,_) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>disj for t u\<close> =
         if b then prod (signed_nclauses b t) (signed_nclauses b u)
              else sum (signed_nclauses b t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.implies\<close>,_) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>implies for t u\<close> =
         if b then prod (signed_nclauses (not b) t) (signed_nclauses b u)
              else sum (signed_nclauses (not b) t) (signed_nclauses b u)
-    | signed_nclauses b (Const(\<^const_name>\<open>HOL.eq\<close>, Type ("fun", [T, _])) $ t $ u) =
+    | signed_nclauses b \<^Const_>\<open>HOL.eq \<open>T\<close> for t u\<close> =
         if T = HOLogic.boolT then (*Boolean equality is if-and-only-if*)
             if b then sum (prod (signed_nclauses (not b) t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) u) (signed_nclauses b t))
                  else sum (prod (signed_nclauses b t) (signed_nclauses b u))
                           (prod (signed_nclauses (not b) t) (signed_nclauses (not b) u))
         else 1
-    | signed_nclauses b (Const(\<^const_name>\<open>Ex\<close>, _) $ Abs (_,_,t)) = signed_nclauses b t
-    | signed_nclauses b (Const(\<^const_name>\<open>All\<close>,_) $ Abs (_,_,t)) = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>Ex _ for \<open>Abs (_,_,t)\<close>\<close> = signed_nclauses b t
+    | signed_nclauses b \<^Const_>\<open>All _ for \<open>Abs (_,_,t)\<close>\<close> = signed_nclauses b t
     | signed_nclauses _ _ = 1; (* literal *)
  in signed_nclauses true t end
 
@@ -351,7 +350,7 @@
   val spec_var =
     Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))))
     |> Thm.term_of |> dest_Var;
-  fun name_of (Const (\<^const_name>\<open>All\<close>, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu;
+  fun name_of \<^Const_>\<open>All _ for \<open>Abs(x, _, _)\<close>\<close> = x | name_of _ = Name.uu;
 in  
   fun freeze_spec th ctxt =
     let
@@ -379,15 +378,15 @@
         else if not (has_conns [\<^const_name>\<open>All\<close>, \<^const_name>\<open>Ex\<close>, \<^const_name>\<open>HOL.conj\<close>] (Thm.prop_of th))
         then nodups ctxt th :: ths (*no work to do, terminate*)
         else case head_of (HOLogic.dest_Trueprop (Thm.concl_of th)) of
-            Const (\<^const_name>\<open>HOL.conj\<close>, _) => (*conjunction*)
+            \<^Const_>\<open>conj\<close> => (*conjunction*)
                 cnf_aux (th RS conjunct1, cnf_aux (th RS conjunct2, ths))
-          | Const (\<^const_name>\<open>All\<close>, _) => (*universal quantifier*)
+          | \<^Const_>\<open>All _\<close> => (*universal quantifier*)
                 let val (th', ctxt') = freeze_spec th (! ctxt_ref)
                 in  ctxt_ref := ctxt'; cnf_aux (th', ths) end
-          | Const (\<^const_name>\<open>Ex\<close>, _) =>
+          | \<^Const_>\<open>Ex _\<close> =>
               (*existential quantifier: Insert Skolem functions*)
               cnf_aux (apply_skolem_theorem (! ctxt_ref) (th, old_skolem_ths), ths)
-          | Const (\<^const_name>\<open>HOL.disj\<close>, _) =>
+          | \<^Const_>\<open>disj\<close> =>
               (*Disjunction of P, Q: Create new goal of proving ?P | ?Q and solve it using
                 all combinations of converting P, Q to CNF.*)
               (*There is one assumption, which gets bound to prem and then normalized via
@@ -415,8 +414,7 @@
 
 (**** Generation of contrapositives ****)
 
-fun is_left (Const (\<^const_name>\<open>Trueprop\<close>, _) $
-               (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ _ $ _) $ _)) = true
+fun is_left \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for \<open>\<^Const_>\<open>disj for _ _\<close>\<close> _\<close>\<close>\<close> = true
   | is_left _ = false;
 
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
@@ -437,8 +435,8 @@
 
 fun rigid t = not (is_Var (head_of t));
 
-fun ok4horn (Const (\<^const_name>\<open>Trueprop\<close>,_) $ (Const (\<^const_name>\<open>HOL.disj\<close>, _) $ t $ _)) = rigid t
-  | ok4horn (Const (\<^const_name>\<open>Trueprop\<close>,_) $ t) = rigid t
+fun ok4horn \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>disj for t _\<close>\<close>\<close> = rigid t
+  | ok4horn \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4horn _ = false;
 
 (*Create a meta-level Horn clause*)
@@ -472,8 +470,7 @@
 
 (***** MESON PROOF PROCEDURE *****)
 
-fun rhyps (Const(\<^const_name>\<open>Pure.imp\<close>,_) $ (Const(\<^const_name>\<open>Trueprop\<close>,_) $ A) $ phi,
-           As) = rhyps(phi, A::As)
+fun rhyps (\<^Const_>\<open>Pure.imp for \<open>\<^Const_>\<open>Trueprop for A\<close>\<close> phi\<close>, As) = rhyps(phi, A::As)
   | rhyps (_, As) = As;
 
 (** Detecting repeated assumptions in a subgoal **)
@@ -517,8 +514,8 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun ok4nnf (Const (\<^const_name>\<open>Trueprop\<close>,_) $ (Const (\<^const_name>\<open>Not\<close>, _) $ t)) = rigid t
-  | ok4nnf (Const (\<^const_name>\<open>Trueprop\<close>,_) $ t) = rigid t
+fun ok4nnf \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for t\<close>\<close>\<close> = rigid t
+  | ok4nnf \<^Const_>\<open>Trueprop for t\<close> = rigid t
   | ok4nnf _ = false;
 
 fun make_nnf1 ctxt th =
@@ -610,7 +607,7 @@
           end
       end
   in
-    if T = \<^typ>\<open>bool\<close> then
+    if T = \<^Type>\<open>bool\<close> then
       NONE
     else case pat t u of
       (SOME T, p as _ $ _) => SOME (Abs (Name.uu, T, p))
@@ -623,12 +620,10 @@
 (* Strengthens "f g ~= f h" to "f g ~= f h & (EX x. g x ~= h x)". *)
 fun cong_extensionalize_thm ctxt th =
   (case Thm.concl_of th of
-    \<^const>\<open>Trueprop\<close> $ (\<^const>\<open>Not\<close>
-        $ (Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _]))
-           $ (t as _ $ _) $ (u as _ $ _))) =>
-    (case get_F_pattern T t u of
-      SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
-    | NONE => th)
+    \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>Not for \<open>\<^Const_>\<open>HOL.eq T for \<open>t as _ $ _\<close> \<open>u as _ $ _\<close>\<close>\<close>\<close>\<close>\<close> =>
+      (case get_F_pattern T t u of
+        SOME p => th RS infer_instantiate ctxt [(("F", 0), Thm.cterm_of ctxt p)] ext_cong_neq
+      | NONE => th)
   | _ => th)
 
 (* Removes the lambdas from an equation of the form "t = (%x1 ... xn. u)". It
@@ -636,9 +631,9 @@
    proof in "Tarski" that relies on the current behavior. *)
 fun abs_extensionalize_conv ctxt ct =
   (case Thm.term_of ct of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Abs _ =>
-    ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
-           then_conv abs_extensionalize_conv ctxt)
+    \<^Const_>\<open>HOL.eq _ for _ \<open>Abs _\<close>\<close> =>
+      ct |> (Conv.rewr_conv @{thm fun_eq_iff [THEN eq_reflection]}
+             then_conv abs_extensionalize_conv ctxt)
   | _ $ _ => Conv.comb_conv (abs_extensionalize_conv ctxt) ct
   | Abs _ => Conv.abs_conv (abs_extensionalize_conv o snd) ctxt ct
   | _ => Conv.all_conv ct)
--- a/src/HOL/Tools/Meson/meson_clausify.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -41,9 +41,9 @@
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   (case Thm.concl_of th of    (*conclusion variable*)
-    \<^const>\<open>Trueprop\<close> $ (Var (v as (_, \<^typ>\<open>bool\<close>))) =>
+    \<^Const_>\<open>Trueprop for \<open>Var (v as (_, \<^Type>\<open>bool\<close>))\<close>\<close> =>
       Thm.instantiate (TVars.empty, Vars.make [(v, cfalse)]) th
-  | Var (v as (_, \<^typ>\<open>prop\<close>)) =>
+  | Var (v as (_, \<^Type>\<open>prop\<close>)) =>
       Thm.instantiate (TVars.empty, Vars.make [(v, ctp_false)]) th
   | _ => th)
 
@@ -51,9 +51,8 @@
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 
 fun mk_old_skolem_term_wrapper t =
-  let val T = fastype_of t in
-    Const (\<^const_name>\<open>Meson.skolem\<close>, T --> T) $ t
-  end
+  let val T = fastype_of t
+  in \<^Const>\<open>Meson.skolem T for t\<close> end
 
 fun beta_eta_in_abs_body (Abs (s, T, t')) = Abs (s, T, beta_eta_in_abs_body t')
   | beta_eta_in_abs_body t = Envir.beta_eta_contract t
@@ -61,7 +60,7 @@
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun old_skolem_defs th =
   let
-    fun dec_sko (Const (\<^const_name>\<open>Ex\<close>, _) $ (body as Abs (_, T, p))) rhss =
+    fun dec_sko \<^Const_>\<open>Ex _ for \<open>body as Abs (_, T, p)\<close>\<close> rhss =
         (*Existential: declare a Skolem function, then insert into body and continue*)
         let
           val args = Misc_Legacy.term_frees body
@@ -72,20 +71,20 @@
             |> mk_old_skolem_term_wrapper
           val comb = list_comb (rhs, args)
         in dec_sko (subst_bound (comb, p)) (rhs :: rhss) end
-      | dec_sko (Const (\<^const_name>\<open>All\<close>,_) $ Abs (a, T, p)) rhss =
+      | dec_sko \<^Const_>\<open>All _ for \<open>Abs (a, T, p)\<close>\<close> rhss =
         (*Universal quant: insert a free variable into body and continue*)
         let val fname = singleton (Name.variant_list (Misc_Legacy.add_term_names (p, []))) a
         in dec_sko (subst_bound (Free(fname,T), p)) rhss end
-      | dec_sko (\<^const>\<open>conj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (\<^const>\<open>disj\<close> $ p $ q) rhss = rhss |> dec_sko p |> dec_sko q
-      | dec_sko (\<^const>\<open>Trueprop\<close> $ p) rhss = dec_sko p rhss
+      | dec_sko \<^Const_>\<open>conj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko \<^Const_>\<open>disj for p q\<close> rhss = rhss |> dec_sko p |> dec_sko q
+      | dec_sko \<^Const_>\<open>Trueprop for p\<close> rhss = dec_sko p rhss
       | dec_sko _ rhss = rhss
   in  dec_sko (Thm.prop_of th) []  end;
 
 
 (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
 
-fun is_quasi_lambda_free (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) = true
+fun is_quasi_lambda_free \<^Const_>\<open>Meson.skolem _ for _\<close> = true
   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false
--- a/src/HOL/Tools/Metis/metis_generate.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_generate.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -71,8 +71,7 @@
 fun conceal_old_skolem_terms i old_skolems t =
   if exists_Const (curry (op =) \<^const_name>\<open>Meson.skolem\<close> o fst) t then
     let
-      fun aux old_skolems
-             (t as (Const (\<^const_name>\<open>Meson.skolem\<close>, Type (_, [_, T])) $ _)) =
+      fun aux old_skolems (t as \<^Const_>\<open>Meson.skolem T for _\<close>) =
           let
             val (old_skolems, s) =
               if i = ~1 then
@@ -114,8 +113,8 @@
       if String.isPrefix lam_lifted_prefix s then
         (case AList.lookup (op =) lifted s of
           SOME t =>
-          Const (\<^const_name>\<open>Metis.lambda\<close>, dummyT)
-          $ map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
+            \<^Const>\<open>Metis.lambda dummyT\<close> $
+              map_types (map_type_tvar (K dummyT)) (reveal_lam_lifted lifted t)
         | NONE => t)
       else
         t
@@ -190,7 +189,7 @@
     end
   | metis_axiom_of_atp _ _ _ _ = raise Fail "not CNF -- expected formula"
 
-fun eliminate_lam_wrappers (Const (\<^const_name>\<open>Metis.lambda\<close>, _) $ t) = eliminate_lam_wrappers t
+fun eliminate_lam_wrappers \<^Const_>\<open>Metis.lambda _ for t\<close> = eliminate_lam_wrappers t
   | eliminate_lam_wrappers (t $ u) = eliminate_lam_wrappers t $ eliminate_lam_wrappers u
   | eliminate_lam_wrappers (Abs (s, T, t)) = Abs (s, T, eliminate_lam_wrappers t)
   | eliminate_lam_wrappers t = t
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -221,10 +221,10 @@
       end
   end
 
-fun s_not (\<^const>\<open>Not\<close> $ t) = t
+fun s_not \<^Const_>\<open>Not for t\<close> = t
   | s_not t = HOLogic.mk_not t
-fun simp_not_not (\<^const>\<open>Trueprop\<close> $ t) = \<^const>\<open>Trueprop\<close> $ simp_not_not t
-  | simp_not_not (\<^const>\<open>Not\<close> $ t) = s_not (simp_not_not t)
+fun simp_not_not \<^Const_>\<open>Trueprop for t\<close> = \<^Const>\<open>Trueprop for \<open>simp_not_not t\<close>\<close>
+  | simp_not_not \<^Const_>\<open>Not for t\<close> = s_not (simp_not_not t)
   | simp_not_not t = t
 
 val normalize_literal = simp_not_not o Envir.eta_contract
@@ -414,7 +414,7 @@
 fun is_metis_literal_genuine (_, (s, _)) =
   not (String.isPrefix class_prefix (Metis_Name.toString s))
 fun is_isabelle_literal_genuine t =
-  (case t of _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _) => false | _ => true)
+  (case t of _ $ \<^Const_>\<open>Meson.skolem _ for _\<close> => false | _ => true)
 
 fun count p xs = fold (fn x => if p x then Integer.add 1 else I) xs 0
 
@@ -660,11 +660,11 @@
 
       fun subst_info_of_prem subgoal_no prem =
         (case prem of
-          _ $ (Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ (_ $ t $ num)) =>
-          let val ax_no = HOLogic.dest_nat num in
-            (ax_no, (subgoal_no,
-                     match_term (nth axioms ax_no |> the |> snd, t)))
-          end
+          _ $ \<^Const_>\<open>Meson.skolem _ for \<open>_ $ t $ num\<close>\<close> =>
+            let val ax_no = HOLogic.dest_nat num in
+              (ax_no, (subgoal_no,
+                       match_term (nth axioms ax_no |> the |> snd, t)))
+            end
         | _ => raise TERM ("discharge_skolem_premises: Malformed premise", [prem]))
 
       fun cluster_of_var_name skolem s =
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -48,12 +48,12 @@
    "t => t". Type tag idempotence is also handled this way. *)
 fun reflexive_or_trivial_of_metis ctxt type_enc sym_tab concealed mth =
   (case hol_clause_of_metis ctxt type_enc sym_tab concealed mth of
-    Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ t =>
+    \<^Const_>\<open>HOL.eq _ for _ t\<close> =>
       let
         val ct = Thm.cterm_of ctxt t
         val cT = Thm.ctyp_of_cterm ct
       in refl |> Thm.instantiate' [SOME cT] [SOME ct] end
-  | Const (\<^const_name>\<open>disj\<close>, _) $ t1 $ t2 =>
+  | \<^Const_>\<open>disj for t1 t2\<close> =>
       (if can HOLogic.dest_not t1 then t2 else t1)
       |> HOLogic.mk_Trueprop |> Thm.cterm_of ctxt |> Thm.trivial
   | _ => raise Fail "expected reflexive or trivial clause")
@@ -94,7 +94,7 @@
                     |> Thm.cterm_of ctxt
                     |> Conv.comb_conv (conv true ctxt))
               else Conv.abs_conv (conv false o snd) ctxt ct
-          | Const (\<^const_name>\<open>Meson.skolem\<close>, _) $ _ => Thm.reflexive ct
+          | \<^Const_>\<open>Meson.skolem _ for _\<close> => Thm.reflexive ct
           | _ => Conv.comb_conv (conv true ctxt) ct)
       val eq_th = conv true ctxt (Thm.cprop_of th)
       (* We replace the equation's left-hand side with a beta-equivalent term
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -45,7 +45,6 @@
   val spass_H2NuVS0 : string
   val spass_H2NuVS0Red2 : string
   val spass_H2SOS : string
-  val is_vampire_noncommercial_license_accepted : unit -> bool option
   val isabelle_scala_function: string list * string list
   val remote_atp : string -> string -> string list -> (string * string) list ->
     (atp_failure * string) list -> atp_formula_role -> (Proof.context -> slice_spec * string) ->
@@ -319,7 +318,7 @@
 val iprover_config : atp_config =
   {exec = (["IPROVER_HOME"], ["iproveropt", "iprover"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn problem => fn _ =>
-     ["--clausifier \"$OLD_VAMPIRE_HOME\"/vampire " ^
+     ["--clausifier \"$VAMPIRE_HOME\"/vampire " ^
       "--clausifier_options \"--mode clausify\" " ^
       "--time_out_real " ^ string_of_real (Time.toReal timeout) ^ " " ^ File.bash_path problem],
    proof_delims = tstp_proof_delims,
@@ -452,31 +451,6 @@
 
 (* Vampire *)
 
-fun is_vampire_noncommercial_license_accepted () =
-  let
-    val flag = Options.default_string \<^system_option>\<open>vampire_noncommercial\<close>
-      |> String.map Char.toLower
-  in
-    if flag = "yes" then
-      SOME true
-    else if flag = "no" then
-      SOME false
-    else
-      NONE
-  end
-
-fun check_vampire_noncommercial () =
-  (case is_vampire_noncommercial_license_accepted () of
-    SOME true => ()
-  | SOME false =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover may be used only for noncommercial applications"))
-  | NONE =>
-    error (Pretty.string_of (Pretty.para
-      "The Vampire prover is not activated; to activate it, set the Isabelle system option \
-      \\"vampire_noncommercial\" to \"yes\" (e.g. via the Isabelle/jEdit menu Plugin Options \
-      \/ Isabelle / General)")))
-
 val vampire_basic_options =
   "--proof tptp --output_axiom_names on" ^
   (if ML_System.platform_is_windows
@@ -488,14 +462,13 @@
 
 val vampire_config : atp_config =
   let
-    val format = TFF (Without_FOOL, Monomorphic)
+    val format = TFF (With_FOOL, Monomorphic)
   in
-    {exec = (["OLD_VAMPIRE_HOME"], ["vampire"]),
+    {exec = (["VAMPIRE_HOME"], ["vampire"]),
      arguments = fn _ => fn full_proofs => fn sos => fn timeout => fn problem => fn _ =>
-       (check_vampire_noncommercial ();
-        [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
+       [vampire_basic_options ^ (if full_proofs then " " ^ vampire_full_proof_options else "") ^
          " -t " ^ string_of_int (to_secs 1 timeout) ^ " --input_file " ^ File.bash_path problem
-         |> sos = sosN ? prefix "--sos on "]),
+         |> sos = sosN ? prefix "--sos on "],
      proof_delims =
        [("=========== Refutation ==========",
          "======= End of refutation =======")] @
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -177,9 +177,7 @@
 
 (* The first ATP of the list is used by Auto Sledgehammer. *)
 fun default_provers_param_value mode ctxt =
-  [cvc4N] @
-  (if is_vampire_noncommercial_license_accepted () = SOME false then [] else [vampireN]) @
-  [z3N, eN, spassN, veritN]
+  [cvc4N, vampireN, z3N, eN, spassN, veritN]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   (* In "try" mode, leave at least one thread to another slow tool (e.g. Nitpick) *)
   |> take (Multithreading.max_threads () - (if mode = Try then 1 else 0))
--- a/src/HOL/Tools/etc/options	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Tools/etc/options	Thu Sep 23 11:26:15 2021 +0200
@@ -32,9 +32,6 @@
 public option sledgehammer_timeout : int = 30
   -- "provers will be interrupted after this time (in seconds)"
 
-public option vampire_noncommercial : string = "unknown"
-  -- "status of Vampire activation for noncommercial use (yes, no, unknown)"
-
 public option SystemOnTPTP : string = "http://www.tptp.org/cgi-bin/SystemOnTPTPFormReply"
   -- "URL for SystemOnTPTP service"
 
--- a/src/HOL/Typerep.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/HOL/Typerep.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -32,8 +32,7 @@
 
 typed_print_translation \<open>
   let
-    fun typerep_tr' ctxt (*"typerep"*)
-            (Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>itself\<close>, [T]), _]))
+    fun typerep_tr' ctxt (*"typerep"*) \<^Type>\<open>fun \<open>\<^Type>\<open>itself T\<close>\<close> _\<close>
             (Const (\<^const_syntax>\<open>Pure.type\<close>, _) :: ts) =
           Term.list_comb
             (Syntax.const \<^syntax_const>\<open>_TYPEREP\<close> $ Syntax_Phases.term_of_typ ctxt T, ts)
@@ -49,10 +48,9 @@
     val sorts = replicate (Sign.arity_number thy tyco) \<^sort>\<open>typerep\<close>;
     val vs = Name.invent_names Name.context "'a" sorts;
     val ty = Type (tyco, map TFree vs);
-    val lhs = Const (\<^const_name>\<open>typerep\<close>, Term.itselfT ty --> \<^typ>\<open>typerep\<close>)
-      $ Free ("T", Term.itselfT ty);
-    val rhs = \<^term>\<open>Typerep\<close> $ HOLogic.mk_literal tyco
-      $ HOLogic.mk_list \<^typ>\<open>typerep\<close> (map (HOLogic.mk_typerep o TFree) vs);
+    val lhs = \<^Const>\<open>typerep ty\<close> $ Free ("T", Term.itselfT ty);
+    val rhs = \<^Const>\<open>Typerep\<close> $ HOLogic.mk_literal tyco
+      $ HOLogic.mk_list \<^Type>\<open>typerep\<close> (map (HOLogic.mk_typerep o TFree) vs);
     val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
   in
     thy
--- a/src/Provers/order_tac.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Provers/order_tac.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -78,68 +78,10 @@
   fun expect _ (SOME x) = x
     | expect f NONE = f ()
 
-  fun matches_skeleton t s = t = Term.dummy orelse
-    (case (t, s) of
-      (t0 $ t1, s0 $ s1) => matches_skeleton t0 s0 andalso matches_skeleton t1 s1
-    | _ => t aconv s)
-
-  fun dest_binop t =
-    let
-      val binop_skel = Term.dummy $ Term.dummy $ Term.dummy
-      val not_binop_skel = Logic_Sig.Not $ binop_skel
-    in
-      if matches_skeleton not_binop_skel t
-        then (case t of (_ $ (t1 $ t2 $ t3)) => (false, (t1, t2, t3)))
-        else if matches_skeleton binop_skel t
-          then (case t of (t1 $ t2 $ t3) => (true, (t1, t2, t3)))
-          else raise TERM ("Not a binop literal", [t])
-    end
-
-  fun find_term t = Library.find_first (fn (t', _) => t' aconv t)
-
-  fun reify_order_atom (eq, le, lt) t reifytab =
-    let
-      val (b, (t0, t1, t2)) =
-        (dest_binop t) handle TERM (_, _) => raise TERM ("Can't reify order literal", [t])
-      val binops = [(eq, EQ), (le, LEQ), (lt, LESS)]
-    in
-      case find_term t0 binops of
-        SOME (_, reified_bop) =>
-          reifytab
-          |> Reifytab.get_var t1 ||> Reifytab.get_var t2
-          |> (fn (v1, (v2, vartab')) =>
-               ((b, reified_bop (Int_of_integer v1, Int_of_integer v2)), vartab'))
-          |>> Atom
-      | NONE => raise TERM ("Can't reify order literal", [t])
-    end
-
-  fun reify consts reify_atom t reifytab =
-    let
-      fun reify' (t1 $ t2) reifytab =
-            let
-              val (t0, ts) = strip_comb (t1 $ t2)
-              val consts_of_arity = filter (fn (_, (_, ar)) => length ts = ar) consts
-            in
-              (case find_term t0 consts_of_arity of
-                SOME (_, (reified_op, _)) => fold_map reify' ts reifytab |>> reified_op
-              | NONE => reify_atom (t1 $ t2) reifytab)
-            end
-        | reify' t reifytab = reify_atom t reifytab
-    in
-      reify' t reifytab
-    end
-
   fun list_curry0 f = (fn [] => f, 0)
   fun list_curry1 f = (fn [x] => f x, 1)
   fun list_curry2 f = (fn [x, y] => f x y, 2)
 
-  fun reify_order_conj ord_ops =
-    let
-      val consts = map (apsnd (list_curry2 o curry)) [(Logic_Sig.conj, And), (Logic_Sig.disj, Or)]
-    in   
-      reify consts (reify_order_atom ord_ops)
-    end
-
   fun dereify_term consts reifytab t =
     let
       fun dereify_term' (App (t1, t2)) = (dereify_term' t1) $ (dereify_term' t2)
@@ -204,7 +146,17 @@
             replay_prf_trm' assmtab p
             |> Drule.infer_instantiate' ctxt [SOME (Thm.cterm_of ctxt (dereify t))]
         | replay_prf_trm' assmtab (AppP (p1, p2)) =
-            apply2 (replay_prf_trm' assmtab) (p2, p1) |> (op COMP)
+            let
+              val thy = Proof_Context.theory_of ctxt
+              val (thm1, thm2) = apply2 (replay_prf_trm' assmtab) (p1, p2)
+              val prem = hd (Thm.prems_of thm1)
+              val (_, tenv) = Pattern.first_order_match thy (prem, Thm.prop_of thm2)
+                                                            (Vartab.empty, Vartab.empty)
+              val inst = Vartab.dest tenv |> map (apsnd (Thm.cterm_of ctxt o snd))
+              val thm1 = Drule.infer_instantiate ctxt inst thm1
+            in
+              thm2 COMP thm1
+            end
         | replay_prf_trm' assmtab (AbsP (reified_t, p)) =
             let
               val t = dereify reified_t
@@ -253,108 +205,134 @@
       replay_prf_trm (replay_conv convs) dereify ctxt thmtab assmtab
     end
 
-  fun is_binop_term t =
-    let
-      fun is_included t = forall (curry (op <>) (t |> fastype_of |> domain_type)) excluded_types
-    in
-      (case dest_binop (Logic_Sig.dest_Trueprop t) of
-        (_, (binop, t1, t2)) =>
-          is_included binop andalso
-          (* Exclude terms with schematic variables since the solver can't deal with them.
-             More specifically, the solver uses Assumption.assume which does not allow schematic
-             variables in the assumed cterm.
-          *)
-          Term.add_var_names (binop $ t1 $ t2) [] = []
-      ) handle TERM (_, _) => false
-    end
+  fun strip_Not (nt $ t) = if nt = Logic_Sig.Not then t else nt $ t
+    | strip_Not t = t
 
-  fun partition_matches ctxt term_of pats ys =
-    let
-      val thy = Proof_Context.theory_of ctxt
-
-      fun find_match t env =
-        Library.get_first (try (fn pat => Pattern.match thy (pat, t) env)) pats
-      
-      fun filter_matches xs = fold (fn x => fn (mxs, nmxs, env) =>
-        case find_match (term_of x) env of
-          SOME env' => (x::mxs, nmxs, env')
-        | NONE => (mxs, x::nmxs, env)) xs ([], [], (Vartab.empty, Vartab.empty))
-
-      fun partition xs =
-        case filter_matches xs of
-          ([], _, _) => []
-        | (mxs, nmxs, env) => (env, mxs) :: partition nmxs
-    in
-      partition ys
-    end
-
-  fun limit_not_less [_, _, lt] ctxt prems =
+  fun limit_not_less [_, _, lt] ctxt decomp_prems =
     let
       val thy = Proof_Context.theory_of ctxt
       val trace = Config.get ctxt order_trace_cfg
       val limit = Config.get ctxt order_split_limit_cfg
 
       fun is_not_less_term t =
-        (case dest_binop (Logic_Sig.dest_Trueprop t) of
-          (false, (t0, _, _)) => Pattern.matches thy (lt, t0)
-        | _ => false)
-        handle TERM _ => false
+        case try Logic_Sig.dest_Trueprop t |> Option.map strip_Not of
+          SOME (binop $ _ $ _) => Pattern.matches thy (lt, binop)
+        | NONE => false
 
-      val not_less_prems = filter (is_not_less_term o Thm.prop_of) prems
+      val not_less_prems = filter (is_not_less_term o Thm.prop_of o fst) decomp_prems
       val _ = if trace andalso length not_less_prems > limit
                 then tracing "order split limit exceeded"
                 else ()
      in
-      filter_out (is_not_less_term o Thm.prop_of) prems @
+      filter_out (is_not_less_term o Thm.prop_of o fst) decomp_prems @
       take limit not_less_prems
      end
+
+  fun decomp [eq, le, lt] ctxt t =
+    let
+      fun is_excluded t = exists (fn ty => ty = fastype_of t) excluded_types
+
+      fun decomp'' (binop $ t1 $ t2) =
+            let
+              open Order_Procedure
+              val thy = Proof_Context.theory_of ctxt
+              fun try_match pat = try (Pattern.match thy (pat, binop)) (Vartab.empty, Vartab.empty)
+            in if is_excluded t1 then NONE
+               else case (try_match eq, try_match le, try_match lt) of
+                      (SOME env, _, _) => SOME (true, EQ, (t1, t2), env)
+                    | (_, SOME env, _) => SOME (true, LEQ, (t1, t2), env)
+                    | (_, _, SOME env) => SOME (true, LESS, (t1, t2), env)
+                    | _ => NONE
+            end
+        | decomp'' _ = NONE
+
+        fun decomp' (nt $ t) =
+              if nt = Logic_Sig.Not
+                then decomp'' t |> Option.map (fn (b, c, p, e) => (not b, c, p, e))
+                else decomp'' (nt $ t)
+          | decomp' t = decomp'' t
+
+    in
+      try Logic_Sig.dest_Trueprop t |> Option.mapPartial decomp'
+    end
+
+  fun maximal_envs envs =
+    let
+      fun test_opt p (SOME x) = p x
+        | test_opt _ NONE = false
+
+      fun leq_env (tyenv1, tenv1) (tyenv2, tenv2) =
+        Vartab.forall (fn (v, ty) =>
+          Vartab.lookup tyenv2 v |> test_opt (fn ty2 => ty2 = ty)) tyenv1
+        andalso
+        Vartab.forall (fn (v, (ty, t)) =>
+          Vartab.lookup tenv2 v |> test_opt (fn (ty2, t2) => ty2 = ty andalso t2 aconv t)) tenv1
+
+      fun fold_env (i, env) es = fold_index (fn (i2, env2) => fn es =>
+        if i = i2 then es else if leq_env env env2 then (i, i2) :: es else es) envs es
+      
+      val env_order = fold_index fold_env envs []
+
+      val graph = fold_index (fn (i, env) => fn g => Int_Graph.new_node (i, env) g)
+                             envs Int_Graph.empty
+      val graph = fold Int_Graph.add_edge env_order graph
+
+      val strong_conns = Int_Graph.strong_conn graph
+      val maximals =
+        filter (fn comp => length comp = length (Int_Graph.all_succs graph comp)) strong_conns
+    in
+      map (Int_Graph.all_preds graph) maximals
+    end
       
   fun order_tac raw_order_proc octxt simp_prems =
     Subgoal.FOCUS (fn {prems=prems, context=ctxt, ...} =>
       let
         val trace = Config.get ctxt order_trace_cfg
 
-        val binop_prems = filter (is_binop_term o Thm.prop_of) (prems @ simp_prems)
-        val strip_binop = (fn (x, _, _) => x) o snd o dest_binop
-        val binop_of = strip_binop o Logic_Sig.dest_Trueprop o Thm.prop_of
+        fun these' _ [] = []
+          | these' f (x :: xs) = case f x of NONE => these' f xs | SOME y => (x, y) :: these' f xs
 
-        (* Due to local_setup, the operators of the order may contain schematic term and type
-           variables. We partition the premises according to distinct instances of those operators.
-         *)
-        val part_prems = partition_matches ctxt binop_of (#ops octxt) binop_prems
-          |> (case #kind octxt of
-                Order => map (fn (env, prems) =>
-                          (env, limit_not_less (#ops octxt) ctxt prems))
-              | _ => I)
-              
+        val prems = filter (fn p => null (Term.add_vars (Thm.prop_of p) [])) (simp_prems @ prems)
+        val decomp_prems = these' (decomp (#ops octxt) ctxt o Thm.prop_of) prems
+
+        fun env_of (_, (_, _, _, env)) = env
+        val env_groups = maximal_envs (map env_of decomp_prems)
+        
         fun order_tac' (_, []) = no_tac
-          | order_tac' (env, prems) =
+          | order_tac' (env, decomp_prems) =
             let
-              val [eq, le, lt] = #ops octxt
-              val subst_contract = Envir.eta_contract o Envir.subst_term env
-              val ord_ops = (subst_contract eq,
-                             subst_contract le,
-                             subst_contract lt)
+              val [eq, le, lt] = #ops octxt |> map (Envir.subst_term env) |> map Envir.eta_contract
+
+              val decomp_prems = case #kind octxt of
+                                   Order => limit_not_less (#ops octxt) ctxt decomp_prems
+                                 | _ => decomp_prems
+      
+              fun reify_prem (_, (b, ctor, (x, y), _)) (ps, reifytab) =
+                (Reifytab.get_var x ##>> Reifytab.get_var y) reifytab
+                |>> (fn vp => (b, ctor (apply2 Int_of_integer vp)) :: ps)
+              val (reified_prems, reifytab) = fold_rev reify_prem decomp_prems ([], Reifytab.empty)
+
+              val _ = if trace then @{print} ([eq, le, lt], reified_prems, prems)
+                               else ([eq, le, lt], reified_prems, prems)
   
-              val _ = if trace then @{print} (ord_ops, prems) else (ord_ops, prems)
-  
-              val prems_conj_thm = foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a]) prems
-                |> Conv.fconv_rule Thm.eta_conversion 
+              val reified_prems_conj = foldl1 (fn (x, a) => And (x, a)) (map Atom reified_prems)
+              val prems_conj_thm = map fst decomp_prems
+                                   |> foldl1 (fn (x, a) => Logic_Sig.conjI OF [x, a])
+                                   |> Conv.fconv_rule Thm.eta_conversion 
               val prems_conj = prems_conj_thm |> Thm.prop_of
-              val (reified_prems_conj, reifytab) =
-                reify_order_conj ord_ops (Logic_Sig.dest_Trueprop prems_conj) Reifytab.empty
-  
+
               val proof = raw_order_proc reified_prems_conj
   
               val assmtab = Termtab.make [(prems_conj, prems_conj_thm)]
-              val replay = replay_order_prf_trm ord_ops octxt ctxt reifytab assmtab
+              val replay = replay_order_prf_trm (eq, le, lt) octxt ctxt reifytab assmtab
             in
               case proof of
                 NONE => no_tac
               | SOME p => SOLVED' (resolve_tac ctxt [replay p]) 1
             end
      in
-      FIRST (map order_tac' part_prems)
+       map (fn is => ` (env_of o hd) (map (nth decomp_prems) is) |> order_tac') env_groups
+       |> FIRST
      end)
 
   val ad_absurdum_tac = SUBGOAL (fn (A, i) =>
@@ -367,11 +345,8 @@
       | NONE => resolve0_tac [Logic_Sig.ccontr] i)
 
   fun tac raw_order_proc octxt simp_prems ctxt =
-      EVERY' [
-          ad_absurdum_tac,
-          CONVERSION Thm.eta_conversion,
-          order_tac raw_order_proc octxt simp_prems ctxt
-        ]
+        EVERY' [ ad_absurdum_tac, CONVERSION Thm.eta_conversion
+               , order_tac raw_order_proc octxt simp_prems ctxt]
   
 end
 
--- a/src/Pure/Admin/build_jdk.scala	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Admin/build_jdk.scala	Thu Sep 23 11:26:15 2021 +0200
@@ -45,7 +45,7 @@
       if (path.is_file) {
         val file_descr = Isabelle_System.bash("file -b " + File.bash_path(path)).check.out
         if (platform_regex.pattern.matcher(file_descr).matches) {
-          val Version = ("^(" + major_version + """\.[0-9.]+\+\d+)(?:-LTS)?$""").r
+          val Version = ("^(" + major_version + """[0-9.+]+)(?:-LTS)?$""").r
           val version_lines =
             Isabelle_System.bash("strings " + File.bash_path(path)).check
               .out_lines.flatMap({ case Version(s) => Some(s) case _ => None })
--- a/src/Pure/Admin/build_release.scala	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Thu Sep 23 11:26:15 2021 +0200
@@ -490,6 +490,7 @@
     context: Release_Context,
     afp_rev: String = "",
     platform_families: List[Platform.Family.Value] = default_platform_families,
+    java_home: Path = default_java_home,
     more_components: List[Path] = Nil,
     website: Option[Path] = None,
     build_sessions: List[String] = Nil,
@@ -703,7 +704,8 @@
                 .replace("\\jdk\\", "\\" + jdk_component + "\\"))
 
             execute(tmp_dir,
-              "\"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
+              "env JAVA_HOME=" + File.bash_platform_path(java_home) +
+              " \"windows_app/launch4j-${ISABELLE_PLATFORM_FAMILY}/launch4j\" isabelle.xml")
 
             Isabelle_System.copy_file(app_template + Path.explode("manifest.xml"),
               isabelle_target + isabelle_exe.ext("manifest"))
@@ -842,12 +844,15 @@
 
   /** command line entry point **/
 
+  def default_java_home: Path = Path.explode("$JAVA_HOME").expand
+
   def main(args: Array[String]): Unit =
   {
     Command_Line.tool {
       var afp_rev = ""
       var components_base: Path = Components.default_components_base
       var target_dir = Path.current
+      var java_home = default_java_home
       var release_name = ""
       var source_archive = ""
       var website: Option[Path] = None
@@ -867,6 +872,7 @@
     -C DIR       base directory for Isabelle components (default: """ +
         Components.default_components_base + """)
     -D DIR       target directory (default ".")
+    -J JAVA_HOME Java version for running launch4j (e.g. version 11)
     -R RELEASE   explicit release name
     -S ARCHIVE   use existing source archive (file or URL)
     -W WEBSITE   produce minimal website in given directory
@@ -883,6 +889,7 @@
         "A:" -> (arg => afp_rev = arg),
         "C:" -> (arg => components_base = Path.explode(arg)),
         "D:" -> (arg => target_dir = Path.explode(arg)),
+        "J:" -> (arg => java_home = Path.explode(arg)),
         "R:" -> (arg => release_name = arg),
         "S:" -> (arg => source_archive = arg),
         "W:" -> (arg => website = Some(Path.explode(arg))),
@@ -929,7 +936,7 @@
         }
 
       build_release(options, context, afp_rev = afp_rev, platform_families = platform_families,
-        more_components = more_components, build_sessions = build_sessions,
+        java_home = java_home, more_components = more_components, build_sessions = build_sessions,
         build_library = build_library, parallel_jobs = parallel_jobs, website = website)
     }
   }
--- a/src/Pure/Admin/isabelle_devel.scala	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Thu Sep 23 11:26:15 2021 +0200
@@ -44,6 +44,7 @@
           val context = Build_Release.Release_Context(target_dir)
           Build_Release.build_release_archive(context, rev)
           Build_Release.build_release(options, context, afp_rev = afp_rev,
+            java_home = Path.explode("$BUILD_JAVA_HOME"),
             build_sessions = List(Isabelle_System.getenv("ISABELLE_LOGIC")),
             website = Some(website_dir))
         })
--- a/src/Pure/Isar/local_theory.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Isar/local_theory.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -60,8 +60,15 @@
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
   val set_defsort: sort -> local_theory -> local_theory
+  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    local_theory -> local_theory
+  val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list ->
+    local_theory -> local_theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
+  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
+    local_theory -> local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
+  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val type_alias: binding -> string -> local_theory -> local_theory
   val const_alias: binding -> string -> local_theory -> local_theory
   val init: {background_naming: Name_Space.naming, setup: theory -> Proof.context,
@@ -297,11 +304,30 @@
     (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
 
 
+(* syntax *)
+
+fun gen_syntax prep_type add mode raw_args lthy =
+  let
+    val args = map (fn (c, T, mx) => (c, prep_type lthy T, mx)) raw_args;
+    val args' = map (fn (c, T, mx) => (c, T, Mixfix.reset_pos mx)) args;
+    val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.syntax add mode args;
+  in
+    declaration {syntax = true, pervasive = false}
+      (fn _ => Proof_Context.generic_syntax add mode args') lthy
+  end;
+
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Proof_Context.read_typ_syntax;
+
+
 (* notation *)
 
-fun type_notation add mode raw_args lthy =
+local
+
+fun gen_type_notation prep_type add mode raw_args lthy =
   let
-    val args = map (apfst (Logic.type_map (Assumption.export_term lthy (target_of lthy)))) raw_args;
+    val prepare = prep_type lthy #> Logic.type_map (Assumption.export_term lthy (target_of lthy));
+    val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.type_notation add mode args;
   in
@@ -309,9 +335,10 @@
       (Proof_Context.generic_type_notation add mode args') lthy
   end;
 
-fun notation add mode raw_args lthy =
+fun gen_notation prep_const add mode raw_args lthy =
   let
-    val args = map (apfst (Assumption.export_term lthy (target_of lthy))) raw_args
+    val prepare = prep_const lthy #> Assumption.export_term lthy (target_of lthy);
+    val args = map (apfst prepare) raw_args;
     val args' = map (apsnd Mixfix.reset_pos) args;
     val _ = lthy |> Context_Position.is_visible lthy ? Proof_Context.notation add mode args;
   in
@@ -319,6 +346,17 @@
       (Proof_Context.generic_notation add mode args') lthy
   end;
 
+in
+
+val type_notation = gen_type_notation (K I);
+val type_notation_cmd =
+  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
+
+val notation = gen_notation (K I);
+val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
+
+end;
+
 
 (* name space aliases *)
 
--- a/src/Pure/Isar/object_logic.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Isar/object_logic.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -11,6 +11,7 @@
   val add_judgment: binding * typ * mixfix -> theory -> theory
   val add_judgment_cmd: binding * string * mixfix -> theory -> theory
   val judgment_name: Proof.context -> string
+  val judgment_const: Proof.context -> string * typ
   val is_judgment: Proof.context -> term -> bool
   val drop_judgment: Proof.context -> term -> term
   val fixed_judgment: Proof.context -> string -> term
@@ -91,10 +92,9 @@
   let
     val c = Sign.full_name thy b;
     val thy' = thy |> add_consts [(b, T, mx)];
-    val T' = Logic.unvarifyT_global (Sign.the_const_type thy' c);
   in
     thy'
-    |> Theory.add_deps_global "" (Theory.const_dep thy' (c, T')) []
+    |> Theory.add_deps_const c
     |> (Context.theory_map o map_data) (fn (base_sort, judgment, atomize_rulify) =>
         if is_some judgment then error "Attempt to redeclare object-logic judgment"
         else (base_sort, SOME c, atomize_rulify))
@@ -115,13 +115,24 @@
     SOME name => name
   | _ => raise TERM ("Unknown object-logic judgment", []));
 
-fun is_judgment ctxt (Const (c, _) $ _) = c = judgment_name ctxt
-  | is_judgment _ _ = false;
+fun judgment_const ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+    val c = judgment_name ctxt;
+    val T = Sign.the_const_type thy c;
+  in (c, T) end;
 
-fun drop_judgment ctxt (Abs (x, T, t)) = Abs (x, T, drop_judgment ctxt t)
-  | drop_judgment ctxt (tm as (Const (c, _) $ t)) =
-      if (c = judgment_name ctxt handle TERM _ => false) then t else tm
-  | drop_judgment _ tm = tm;
+fun is_judgment ctxt =
+  let val name = judgment_name ctxt
+  in fn Const (c, _) $ _ => c = name | _ => false end;
+
+fun drop_judgment ctxt =
+  let
+    val name = judgment_name ctxt;
+    fun drop (Abs (x, T, t)) = Abs (x, T, drop t)
+      | drop (t as Const (c, _) $ u) = if c = name then u else t
+      | drop t = t;
+  in drop end handle TERM _ => I;
 
 fun fixed_judgment ctxt x =
   let  (*be robust wrt. low-level errors*)
--- a/src/Pure/Isar/proof_context.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -155,6 +155,11 @@
   val apply_case: Rule_Cases.T -> Proof.context -> (string * term list) list * Proof.context
   val check_case: Proof.context -> bool ->
     string * Position.T -> binding option list -> Rule_Cases.T
+  val check_syntax_const: Proof.context -> string * Position.T -> string
+  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    Proof.context -> Proof.context
+  val generic_syntax: bool -> Syntax.mode -> (string * typ * mixfix) list ->
+    Context.generic -> Context.generic
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> Proof.context -> Proof.context
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> Proof.context -> Proof.context
   val generic_type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> morphism ->
@@ -1123,6 +1128,20 @@
 end;
 
 
+(* syntax *)
+
+fun check_syntax_const ctxt (c, pos) =
+  if is_some (Syntax.lookup_const (syn_of ctxt) c) then c
+  else error ("Unknown syntax const: " ^ quote c ^ Position.here pos);
+
+fun syntax add mode args ctxt =
+  let val args' = map (pair Local_Syntax.Const) args
+  in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end;
+
+fun generic_syntax add mode args =
+  Context.mapping (Sign.syntax add mode args) (syntax add mode args);
+
+
 (* notation *)
 
 local
@@ -1138,9 +1157,9 @@
       | NONE => NONE)
   | const_syntax _ _ = NONE;
 
-fun gen_notation syntax add mode args ctxt =
+fun gen_notation make_syntax add mode args ctxt =
   ctxt |> map_syntax_idents
-    (Local_Syntax.update_modesyntax ctxt add mode (map_filter (syntax ctxt) args));
+    (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args));
 
 in
 
--- a/src/Pure/Isar/specification.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -46,11 +46,6 @@
   val alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
   val type_alias: binding * string -> local_theory -> local_theory
   val type_alias_cmd: binding * (xstring * Position.T) -> local_theory -> local_theory
-  val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
-  val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list ->
-    local_theory -> local_theory
-  val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
-  val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
   val theorems: string ->
     (Attrib.binding * Attrib.thms) list ->
     (binding * typ option * mixfix) list ->
@@ -334,28 +329,6 @@
   gen_alias Local_Theory.type_alias (apfst (#1 o dest_Type) ooo Proof_Context.check_type_name);
 
 
-(* notation *)
-
-local
-
-fun gen_type_notation prep_type add mode args lthy =
-  lthy |> Local_Theory.type_notation add mode (map (apfst (prep_type lthy)) args);
-
-fun gen_notation prep_const add mode args lthy =
-  lthy |> Local_Theory.notation add mode (map (apfst (prep_const lthy)) args);
-
-in
-
-val type_notation = gen_type_notation (K I);
-val type_notation_cmd =
-  gen_type_notation (Proof_Context.read_type_name {proper = true, strict = false});
-
-val notation = gen_notation (K I);
-val notation_cmd = gen_notation (Proof_Context.read_const {proper = false, strict = false});
-
-end;
-
-
 (* fact statements *)
 
 local
--- a/src/Pure/ML/ml_antiquotations1.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -4,7 +4,13 @@
 Miscellaneous ML antiquotations: part 1.
 *)
 
-structure ML_Antiquotations1: sig end =
+signature ML_ANTIQUOTATIONS1 =
+sig
+  val make_judgment: Proof.context -> term -> term
+  val dest_judgment: Proof.context -> term -> term
+end;
+
+structure ML_Antiquotations1: ML_ANTIQUOTATIONS1 =
 struct
 
 (* ML support *)
@@ -171,10 +177,8 @@
     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
-    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
-      if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
-      then ML_Syntax.print_string c
-      else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #>
+    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, arg) =>
+      ML_Syntax.print_string (Proof_Context.check_syntax_const ctxt arg))) #>
 
   ML_Antiquotation.inline_embedded \<^binding>\<open>const\<close>
     (Args.context -- Scan.lift (Parse.position Args.embedded_inner_syntax) -- Scan.optional
@@ -192,6 +196,29 @@
         in ML_Syntax.atomic (ML_Syntax.print_term const) end)));
 
 
+(* object-logic judgment *)
+
+fun make_judgment ctxt =
+  let val const = Object_Logic.judgment_const ctxt
+  in fn t => Const const $ t end;
+
+fun dest_judgment ctxt =
+  let
+    val is_judgment = Object_Logic.is_judgment ctxt;
+    val drop_judgment = Object_Logic.drop_judgment ctxt;
+  in
+    fn t =>
+      if is_judgment t then drop_judgment t
+      else raise TERM ("dest_judgment", [t])
+  end;
+
+val _ = Theory.setup
+ (ML_Antiquotation.value \<^binding>\<open>make_judgment\<close>
+   (Scan.succeed "ML_Antiquotations1.make_judgment ML_context") #>
+  ML_Antiquotation.value \<^binding>\<open>dest_judgment\<close>
+   (Scan.succeed "ML_Antiquotations1.dest_judgment ML_context"));
+
+
 (* type/term constructors *)
 
 local
--- a/src/Pure/Proof/proof_syntax.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -46,7 +46,7 @@
   |> Sign.add_nonterminals_global
     [Binding.make ("param", \<^here>),
      Binding.make ("params", \<^here>)]
-  |> Sign.add_syntax Syntax.mode_default
+  |> Sign.syntax true Syntax.mode_default
     [("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
      ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
      ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
--- a/src/Pure/Pure.thy	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/Pure.thy	Thu Sep 23 11:26:15 2021 +0200
@@ -384,14 +384,14 @@
     (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
+  Outer_Syntax.local_theory \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
+      >> uncurry (Local_Theory.syntax_cmd true));
 
 val _ =
-  Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
+  Outer_Syntax.local_theory \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
     (Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
-      >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
+      >> uncurry (Local_Theory.syntax_cmd false));
 
 val trans_pat =
   Scan.optional
@@ -499,25 +499,25 @@
   Outer_Syntax.local_theory \<^command_keyword>\<open>type_notation\<close>
     "add concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd true mode args));
+      >> (fn (mode, args) => Local_Theory.type_notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_type_notation\<close>
     "delete concrete syntax for type constructors"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.type_notation_cmd false mode args));
+      >> (fn (mode, args) => Local_Theory.type_notation_cmd false mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>notation\<close>
     "add concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd true mode args));
+      >> (fn (mode, args) => Local_Theory.notation_cmd true mode args));
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_notation\<close>
     "delete concrete syntax for constants / fixed variables"
     (Parse.syntax_mode -- Parse.and_list1 (Parse.const -- Parse.mixfix)
-      >> (fn (mode, args) => Specification.notation_cmd false mode args));
+      >> (fn (mode, args) => Local_Theory.notation_cmd false mode args));
 
 in end\<close>
 
--- a/src/Pure/ROOT.scala	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/ROOT.scala	Thu Sep 23 11:26:15 2021 +0200
@@ -21,4 +21,3 @@
   val proper_string = Library.proper_string _
   def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
 }
-
--- a/src/Pure/System/isabelle_system.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/System/isabelle_system.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -180,6 +180,7 @@
 
 fun isabelle_name () = getenv_strict "ISABELLE_NAME";
 
-fun identification () = "Isabelle/" ^ isabelle_id () ^ isabelle_heading ();
+fun identification () =
+  "Isabelle" ^ (case try isabelle_id () of SOME id => "/" ^ id | NONE => "") ^ isabelle_heading ();
 
 end;
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Sep 23 11:26:15 2021 +0200
@@ -139,7 +139,8 @@
 
   def isabelle_name(): String = getenv_strict("ISABELLE_NAME")
 
-  def identification(): String = "Isabelle/" + isabelle_id() + isabelle_heading()
+  def identification(): String =
+    "Isabelle" + (try { "/" + isabelle_id () } catch { case ERROR(_) => "" }) + isabelle_heading()
 
 
   /** file-system operations **/
--- a/src/Pure/pure_thy.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/pure_thy.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -29,18 +29,6 @@
 fun infixr_ (sy, p) = Infixr (Input.string sy, p, Position.no_range);
 fun binder (sy, p, q) = Binder (Input.string sy, p, q, Position.no_range);
 
-fun add_deps_type c thy =
-  let
-    val n = Sign.arity_number thy c;
-    val typargs = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
-  in thy |> Theory.add_deps_global "" ((Defs.Type, c), typargs) [] end
-
-fun add_deps_const c thy =
-  let
-    val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
-    val typargs = Sign.const_typargs thy (c, T);
-  in thy |> Theory.add_deps_global "" ((Defs.Const, c), typargs) [] end;
-
 
 (* application syntax variants *)
 
@@ -68,8 +56,8 @@
 
 val old_appl_syntax_setup =
   Old_Appl_Syntax.put true #>
-  Sign.del_syntax Syntax.mode_default applC_syntax #>
-  Sign.add_syntax Syntax.mode_default appl_syntax;
+  Sign.syntax false Syntax.mode_default applC_syntax #>
+  Sign.syntax true Syntax.mode_default appl_syntax;
 
 
 (* main content *)
@@ -86,11 +74,11 @@
     (Binding.make ("itself", \<^here>), 1, NoSyn),
     (Binding.make ("dummy", \<^here>), 0, NoSyn),
     (qualify (Binding.make ("proof", \<^here>)), 0, NoSyn)]
-  #> add_deps_type "fun"
-  #> add_deps_type "prop"
-  #> add_deps_type "itself"
-  #> add_deps_type "dummy"
-  #> add_deps_type "Pure.proof"
+  #> Theory.add_deps_type "fun"
+  #> Theory.add_deps_type "prop"
+  #> Theory.add_deps_type "itself"
+  #> Theory.add_deps_type "dummy"
+  #> Theory.add_deps_type "Pure.proof"
   #> Sign.add_nonterminals_global
     (map (fn name => Binding.make (name, \<^here>))
       (Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
@@ -100,8 +88,8 @@
         "tvar_position", "id_position", "longid_position", "var_position",
         "str_position", "string_position", "cartouche_position", "type_name",
         "class_name"]))
-  #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
-  #> Sign.add_syntax Syntax.mode_default
+  #> Sign.syntax true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+  #> Sign.syntax true Syntax.mode_default
    [("",            typ "prop' \<Rightarrow> prop",               Mixfix.mixfix "_"),
     ("",            typ "logic \<Rightarrow> any",                Mixfix.mixfix "_"),
     ("",            typ "prop' \<Rightarrow> any",                Mixfix.mixfix "_"),
@@ -197,8 +185,8 @@
     ("_sort_constraint", typ "type \<Rightarrow> prop",           Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
     (const "Pure.term", typ "logic \<Rightarrow> prop",           Mixfix.mixfix "TERM _"),
     (const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
-  #> Sign.add_syntax Syntax.mode_default applC_syntax
-  #> Sign.add_syntax (Print_Mode.ASCII, true)
+  #> Sign.syntax true Syntax.mode_default applC_syntax
+  #> Sign.syntax true (Print_Mode.ASCII, true)
    [(tycon "fun",         typ "type \<Rightarrow> type \<Rightarrow> type",   mixfix ("(_/ => _)", [1, 0], 0)),
     ("_bracket",          typ "types \<Rightarrow> type \<Rightarrow> type",  mixfix ("([_]/ => _)", [0, 0], 0)),
     ("_lambda",           typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic",  mixfix ("(3%_./ _)", [0, 3], 3)),
@@ -208,7 +196,7 @@
     ("_DDDOT",            typ "aprop",                  Mixfix.mixfix "..."),
     ("_bigimpl",          typ "asms \<Rightarrow> prop \<Rightarrow> prop",   mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
     ("_DDDOT",            typ "logic",                  Mixfix.mixfix "...")]
-  #> Sign.add_syntax ("", false)
+  #> Sign.syntax true ("", false)
    [(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
   #> Sign.add_consts
    [(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),
@@ -225,11 +213,11 @@
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("PClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
-  #> add_deps_const "Pure.eq"
-  #> add_deps_const "Pure.imp"
-  #> add_deps_const "Pure.all"
-  #> add_deps_const "Pure.type"
-  #> add_deps_const "Pure.dummy_pattern"
+  #> Theory.add_deps_const "Pure.eq"
+  #> Theory.add_deps_const "Pure.imp"
+  #> Theory.add_deps_const "Pure.all"
+  #> Theory.add_deps_const "Pure.type"
+  #> Theory.add_deps_const "Pure.dummy_pattern"
   #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
   #> Sign.parse_translation Syntax_Trans.pure_parse_translation
   #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
--- a/src/Pure/sign.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/sign.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -72,10 +72,8 @@
   val add_nonterminals: Proof.context -> binding list -> theory -> theory
   val add_nonterminals_global: binding list -> theory -> theory
   val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
-  val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
-  val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
-  val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
-  val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+  val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+  val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
@@ -369,19 +367,15 @@
 
 (* modify syntax *)
 
-fun gen_syntax change_gram parse_typ mode args thy =
+fun gen_syntax parse_typ add mode args thy =
   let
     val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
     fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
       handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
-  in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
-
-fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
+  in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end;
 
-val add_syntax = gen_add_syntax (K I);
-val add_syntax_cmd = gen_add_syntax Syntax.read_typ;
-val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I);
-val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Syntax.read_typ;
 
 fun type_notation add mode args =
   let
@@ -397,7 +391,7 @@
             SOME T => SOME (Lexicon.mark_const c, T, mx)
           | NONE => NONE)
       | const_syntax _ = NONE;
-  in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
+  in syntax add mode (map_filter const_syntax args) thy end;
 
 
 (* add constants *)
@@ -418,7 +412,7 @@
   in
     thy
     |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
-    |> add_syntax Syntax.mode_default (map #2 args)
+    |> syntax true Syntax.mode_default (map #2 args)
     |> pair (map #3 args)
   end;
 
--- a/src/Pure/theory.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Pure/theory.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -30,6 +30,8 @@
   val type_dep: string * typ list -> Defs.entry
   val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory
   val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory
+  val add_deps_const: string -> theory -> theory
+  val add_deps_type: string -> theory -> theory
   val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory
   val specify_const: (binding * typ) * mixfix -> theory -> term * theory
   val check_overloading: Proof.context -> bool -> string * typ -> unit
@@ -270,6 +272,16 @@
 fun add_deps_global a x y thy =
   add_deps (Defs.global_context thy) a x y thy;
 
+fun add_deps_const c thy =
+  let val T = Logic.unvarifyT_global (Sign.the_const_type thy c);
+  in thy |> add_deps_global "" (const_dep thy (c, T)) [] end;
+
+fun add_deps_type c thy =
+  let
+    val n = Sign.arity_number thy c;
+    val args = map (fn a => TFree (a, [])) (Name.invent Name.context Name.aT n);
+  in thy |> add_deps_global "" (type_dep (c, args)) [] end
+
 fun specify_const decl thy =
   let val (t, thy') = Sign.declare_const_global decl thy;
   in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end;
--- a/src/Tools/Setup/src/Build.java	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/Tools/Setup/src/Build.java	Thu Sep 23 11:26:15 2021 +0200
@@ -255,7 +255,7 @@
         }
         if (scala_sources) {
             boolean ok = new MainClass().process(args.toArray(String[]::new));
-            if (!ok) { throw new RuntimeException("Failed to compiler Scala sources"); }
+            if (!ok) { throw new RuntimeException("Failed to compile Scala sources"); }
         }
     }
 
--- a/src/ZF/Tools/datatype_package.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -270,7 +270,7 @@
   (*Each equation has the form
     case(f_con1,...,f_conn)(coni(args)) = f_coni(args) *)
   fun mk_case_eqn (((_,T,_), name, args, _), case_free) =
-    FOLogic.mk_Trueprop
+    \<^make_judgment>
       (FOLogic.mk_eq
        (case_tm $
          (list_comb (Const (Sign.intern_const thy1 name,T),
@@ -320,7 +320,7 @@
           where REC = recursor(f_con1,...,f_conn) and rec_arg is a recursive
           constructor argument.*)
         fun mk_recursor_eqn (((_,T,_), name, args, _), recursor_case) =
-          FOLogic.mk_Trueprop
+          \<^make_judgment>
            (FOLogic.mk_eq
             (recursor_tm $
              (list_comb (Const (Sign.intern_const thy2 name,T),
--- a/src/ZF/Tools/ind_cases.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/Tools/ind_cases.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -33,7 +33,7 @@
 
     fun err msg = cat_error msg ("Malformed set membership statement: " ^ s);
     val A = Syntax.read_prop ctxt s handle ERROR msg => err msg;
-    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (FOLogic.dest_Trueprop
+    val c = #1 (Term.dest_Const (Term.head_of (#2 (Ind_Syntax.dest_mem (\<^dest_judgment>
       (Logic.strip_imp_concl A)))))) handle TERM _ => err "";
   in
     (case Symtab.lookup (IndCasesData.get thy) c of
--- a/src/ZF/Tools/induct_tacs.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/Tools/induct_tacs.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -72,7 +72,7 @@
 fun find_tname ctxt var As =
   let fun mk_pair \<^Const_>\<open>mem for \<open>Free (v,_)\<close> A\<close> = (v, #1 (dest_Const (head_of A)))
         | mk_pair _ = raise Match
-      val pairs = map_filter (try (mk_pair o FOLogic.dest_Trueprop)) As
+      val pairs = map_filter (try (mk_pair o \<^dest_judgment>)) As
       val x =
         (case try (dest_Free o Syntax.read_term ctxt) var of
           SOME (x, _) => x
@@ -101,7 +101,7 @@
     val \<^Const_>\<open>mem for \<open>Var(ixn,_)\<close> _\<close> =
         (case Thm.prems_of rule of
              [] => error "induction is not available for this datatype"
-           | major::_ => FOLogic.dest_Trueprop major)
+           | major::_ => \<^dest_judgment> major)
   in
     Rule_Insts.eres_inst_tac ctxt [((ixn, Position.none), var)] fixes rule i
   end
@@ -124,9 +124,9 @@
                               Syntax.string_of_term_global thy eqn);
 
     val constructors =
-        map (head_of o const_of o FOLogic.dest_Trueprop o Thm.prop_of) case_eqns;
+        map (head_of o const_of o \<^dest_judgment> o Thm.prop_of) case_eqns;
 
-    val \<^Const_>\<open>mem for _ data\<close> = FOLogic.dest_Trueprop (hd (Thm.prems_of elim));
+    val \<^Const_>\<open>mem for _ data\<close> = \<^dest_judgment> (hd (Thm.prems_of elim));
 
     val Const(big_rec_name, _) = head_of data;
 
--- a/src/ZF/Tools/inductive_package.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -185,7 +185,7 @@
   val dummy = writeln "  Proving monotonicity...";
 
   val bnd_mono0 =
-    Goal.prove_global thy1 [] [] (FOLogic.mk_Trueprop (Fp.bnd_mono $ dom_sum $ fp_abs))
+    Goal.prove_global thy1 [] [] (\<^make_judgment> (Fp.bnd_mono $ dom_sum $ fp_abs))
       (fn {context = ctxt, ...} => EVERY
         [resolve_tac ctxt [@{thm Collect_subset} RS @{thm bnd_monoI}] 1,
          REPEAT (ares_tac ctxt (@{thms basic_monos} @ monos) 1)]);
@@ -300,7 +300,7 @@
         prem is a premise of an intr rule*)
      fun add_induct_prem ind_alist (prem as \<^Const_>\<open>Trueprop for \<open>\<^Const_>\<open>mem for t X\<close>\<close>\<close>, iprems) =
           (case AList.lookup (op aconv) ind_alist X of
-               SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
+               SOME pred => prem :: \<^make_judgment> (pred $ t) :: iprems
              | NONE => (*possibly membership in M(rec_tm), for M monotone*)
                  let fun mk_sb (rec_tm,pred) =
                              (rec_tm, \<^Const>\<open>Collect\<close> $ rec_tm $ pred)
@@ -314,7 +314,7 @@
                               (Logic.strip_imp_prems intr)
            val (t,X) = Ind_Syntax.rule_concl intr
            val (SOME pred) = AList.lookup (op aconv) ind_alist X
-           val concl = FOLogic.mk_Trueprop (pred $ t)
+           val concl = \<^make_judgment> (pred $ t)
        in fold_rev Logic.all xs (Logic.list_implies (iprems,concl)) end
        handle Bind => error"Recursion term not found in conclusion";
 
@@ -349,7 +349,7 @@
 
      val quant_induct =
        Goal.prove_global thy4 [] ind_prems
-         (FOLogic.mk_Trueprop (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
+         (\<^make_judgment> (Ind_Syntax.mk_all_imp (big_rec_tm, pred)))
          (fn {context = ctxt, prems} => EVERY
            [rewrite_goals_tac ctxt part_rec_defs,
             resolve_tac ctxt [@{thm impI} RS @{thm allI}] 1,
@@ -404,14 +404,14 @@
 
      (*To instantiate the main induction rule*)
      val induct_concl =
-         FOLogic.mk_Trueprop
+         \<^make_judgment>
            (Ind_Syntax.mk_all_imp
             (big_rec_tm,
              Abs("z", \<^Type>\<open>i\<close>,
                  Balanced_Tree.make FOLogic.mk_conj
                  (ListPair.map mk_rec_imp (rec_tms, preds)))))
      and mutual_induct_concl =
-      FOLogic.mk_Trueprop (Balanced_Tree.make FOLogic.mk_conj qconcls);
+       \<^make_judgment> (Balanced_Tree.make FOLogic.mk_conj qconcls);
 
      val dummy = if !Ind_Syntax.trace then
                  (writeln ("induct_concl = " ^
--- a/src/ZF/Tools/primrec_package.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/Tools/primrec_package.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -18,7 +18,7 @@
 exception RecError of string;
 
 (*Remove outer Trueprop and equality sign*)
-val dest_eqn = FOLogic.dest_eq o FOLogic.dest_Trueprop;
+val dest_eqn = FOLogic.dest_eq o \<^dest_judgment>;
 
 fun primrec_err s = error ("Primrec definition error:\n" ^ s);
 
--- a/src/ZF/arith_data.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/arith_data.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -53,15 +53,13 @@
 
 (*We remove equality assumptions because they confuse the simplifier and
   because only type-checking assumptions are necessary.*)
-fun is_eq_thm th =
-    can FOLogic.dest_eq (FOLogic.dest_Trueprop (Thm.prop_of th));
+fun is_eq_thm th = can FOLogic.dest_eq (\<^dest_judgment> (Thm.prop_of th));
 
 fun prove_conv name tacs ctxt prems (t,u) =
   if t aconv u then NONE
   else
   let val prems' = filter_out is_eq_thm prems
-      val goal = Logic.list_implies (map Thm.prop_of prems',
-        FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
+      val goal = Logic.list_implies (map Thm.prop_of prems', \<^make_judgment> (mk_eq_iff (t, u)));
   in SOME (prems' MRS Goal.prove ctxt [] [] goal (K (EVERY tacs)))
       handle ERROR msg =>
         (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); NONE)
--- a/src/ZF/ind_syntax.ML	Tue Sep 21 14:54:53 2021 +0200
+++ b/src/ZF/ind_syntax.ML	Thu Sep 23 11:26:15 2021 +0200
@@ -79,9 +79,8 @@
   let
     fun mk_intr ((id,T,syn), name, args, prems) =
       Logic.list_implies
-        (map FOLogic.mk_Trueprop prems,
-         FOLogic.mk_Trueprop
-            (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
+        (map \<^make_judgment> prems,
+         \<^make_judgment> (\<^Const>\<open>mem\<close> $ list_comb (Const (Sign.full_bname sg name, T), args) $ rec_tm))
   in  map mk_intr constructs  end;
 
 fun mk_all_intr_tms sg arg = flat (ListPair.map (mk_intr_tms sg) arg);