diff --git a/Admin/components/bundled-windows b/Admin/components/bundled-windows
--- a/Admin/components/bundled-windows
+++ b/Admin/components/bundled-windows
@@ -1,3 +1,3 @@
 #additional components to be bundled for release
-cygwin-20201130
+cygwin-20211002
 windows_app-20181006
diff --git a/src/CCL/CCL.thy b/src/CCL/CCL.thy
--- a/src/CCL/CCL.thy
+++ b/src/CCL/CCL.thy
@@ -1,497 +1,497 @@
 (*  Title:      CCL/CCL.thy
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Classical Computational Logic for Untyped Lambda Calculus
   with reduction to weak head-normal form\<close>
 
 theory CCL
 imports Gfp
 begin
 
 text \<open>
   Based on FOL extended with set collection, a primitive higher-order
   logic.  HOL is too strong - descriptions prevent a type of programs
   being defined which contains only executable terms.
 \<close>
 
 class prog = "term"
 default_sort prog
 
 instance "fun" :: (prog, prog) prog ..
 
 typedecl i
 instance i :: prog ..
 
 
 consts
   (*** Evaluation Judgement ***)
   Eval      ::       "[i,i]\<Rightarrow>prop"          (infixl "\<longlongrightarrow>" 20)
 
   (*** Bisimulations for pre-order and equality ***)
   po          ::       "['a,'a]\<Rightarrow>o"           (infixl "[=" 50)
 
   (*** Term Formers ***)
   true        ::       "i"
   false       ::       "i"
   pair        ::       "[i,i]\<Rightarrow>i"             ("(1<_,/_>)")
   lambda      ::       "(i\<Rightarrow>i)\<Rightarrow>i"            (binder "lam " 55)
   "case"      ::       "[i,i,i,[i,i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   "apply"     ::       "[i,i]\<Rightarrow>i"             (infixl "`" 56)
   bot         ::       "i"
 
   (******* EVALUATION SEMANTICS *******)
 
   (**  This is the evaluation semantics from which the axioms below were derived.  **)
   (**  It is included here just as an evaluator for FUN and has no influence on    **)
   (**  inference in the theory CCL.                                                **)
 
 axiomatization where
   trueV:       "true \<longlongrightarrow> true" and
   falseV:      "false \<longlongrightarrow> false" and
   pairV:       "<a,b> \<longlongrightarrow> <a,b>" and
   lamV:        "\<And>b. lam x. b(x) \<longlongrightarrow> lam x. b(x)" and
 
   caseVtrue:   "\<lbrakk>t \<longlongrightarrow> true; d \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVfalse:  "\<lbrakk>t \<longlongrightarrow> false; e \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVpair:   "\<lbrakk>t \<longlongrightarrow> <a,b>; f(a,b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c" and
   caseVlam:    "\<And>b. \<lbrakk>t \<longlongrightarrow> lam x. b(x); g(b) \<longlongrightarrow> c\<rbrakk> \<Longrightarrow> case(t,d,e,f,g) \<longlongrightarrow> c"
 
   (*** Properties of evaluation: note that "t \<longlongrightarrow> c" impies that c is canonical ***)
 
 axiomatization where
   canonical:  "\<lbrakk>t \<longlongrightarrow> c; c==true \<Longrightarrow> u\<longlongrightarrow>v;
                           c==false \<Longrightarrow> u\<longlongrightarrow>v;
                     \<And>a b. c==<a,b> \<Longrightarrow> u\<longlongrightarrow>v;
                       \<And>f. c==lam x. f(x) \<Longrightarrow> u\<longlongrightarrow>v\<rbrakk> \<Longrightarrow>
              u\<longlongrightarrow>v"
 
   (* Should be derivable - but probably a bitch! *)
 axiomatization where
   substitute: "\<lbrakk>a==a'; t(a)\<longlongrightarrow>c(a)\<rbrakk> \<Longrightarrow> t(a')\<longlongrightarrow>c(a')"
 
   (************** LOGIC ***************)
 
   (*** Definitions used in the following rules ***)
 
 axiomatization where
   bot_def:         "bot == (lam x. x`x)`(lam x. x`x)" and
   apply_def:     "f ` t == case(f, bot, bot, \<lambda>x y. bot, \<lambda>u. u(t))"
 
 definition "fix" :: "(i\<Rightarrow>i)\<Rightarrow>i"
   where "fix(f) == (lam x. f(x`x))`(lam x. f(x`x))"
 
   (*  The pre-order ([=) is defined as a simulation, and behavioural equivalence (=) *)
   (*  as a bisimulation.  They can both be expressed as (bi)simulations up to        *)
   (*  behavioural equivalence (ie the relations PO and EQ defined below).            *)
 
 definition SIM :: "[i,i,i set]\<Rightarrow>o"
   where
   "SIM(t,t',R) ==  (t=true \<and> t'=true) | (t=false \<and> t'=false) |
                   (\<exists>a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : R \<and> <b,b'> : R) |
                   (\<exists>f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
 
 definition POgen :: "i set \<Rightarrow> i set"
   where "POgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot | SIM(t,t',R))}"
 
 definition EQgen :: "i set \<Rightarrow> i set"
   where "EQgen(R) == {p. \<exists>t t'. p=<t,t'> \<and> (t = bot \<and> t' = bot | SIM(t,t',R))}"
 
 definition PO :: "i set"
   where "PO == gfp(POgen)"
 
 definition EQ :: "i set"
   where "EQ == gfp(EQgen)"
 
 
   (*** Rules ***)
 
   (** Partial Order **)
 
 axiomatization where
   po_refl:        "a [= a" and
   po_trans:       "\<lbrakk>a [= b;  b [= c\<rbrakk> \<Longrightarrow> a [= c" and
   po_cong:        "a [= b \<Longrightarrow> f(a) [= f(b)" and
 
   (* Extend definition of [= to program fragments of higher type *)
   po_abstractn:   "(\<And>x. f(x) [= g(x)) \<Longrightarrow> (\<lambda>x. f(x)) [= (\<lambda>x. g(x))"
 
   (** Equality - equivalence axioms inherited from FOL.thy   **)
   (**          - congruence of "=" is axiomatised implicitly **)
 
 axiomatization where
   eq_iff:         "t = t' \<longleftrightarrow> t [= t' \<and> t' [= t"
 
   (** Properties of canonical values given by greatest fixed point definitions **)
 
 axiomatization where
   PO_iff:         "t [= t' \<longleftrightarrow> <t,t'> : PO" and
   EQ_iff:         "t =  t' \<longleftrightarrow> <t,t'> : EQ"
 
   (** Behaviour of non-canonical terms (ie case) given by the following beta-rules **)
 
 axiomatization where
   caseBtrue:            "case(true,d,e,f,g) = d" and
   caseBfalse:          "case(false,d,e,f,g) = e" and
   caseBpair:           "case(<a,b>,d,e,f,g) = f(a,b)" and
   caseBlam:       "\<And>b. case(lam x. b(x),d,e,f,g) = g(b)" and
   caseBbot:              "case(bot,d,e,f,g) = bot"           (* strictness *)
 
   (** The theory is non-trivial **)
 axiomatization where
   distinctness:   "\<not> lam x. b(x) = bot"
 
   (*** Definitions of Termination and Divergence ***)
 
 definition Dvg :: "i \<Rightarrow> o"
   where "Dvg(t) == t = bot"
 
 definition Trm :: "i \<Rightarrow> o"
   where "Trm(t) == \<not> Dvg(t)"
 
 text \<open>
 Would be interesting to build a similar theory for a typed programming language:
     ie.     true :: bool,      fix :: ('a\<Rightarrow>'a)\<Rightarrow>'a  etc......
 
 This is starting to look like LCF.
 What are the advantages of this approach?
         - less axiomatic
         - wfd induction / coinduction and fixed point induction available
 \<close>
 
 
 lemmas ccl_data_defs = apply_def fix_def
 
 declare po_refl [simp]
 
 
 subsection \<open>Congruence Rules\<close>
 
 (*similar to AP_THM in Gordon's HOL*)
 lemma fun_cong: "(f::'a\<Rightarrow>'b) = g \<Longrightarrow> f(x)=g(x)"
   by simp
 
 (*similar to AP_TERM in Gordon's HOL and FOL's subst_context*)
 lemma arg_cong: "x=y \<Longrightarrow> f(x)=f(y)"
   by simp
 
 lemma abstractn: "(\<And>x. f(x) = g(x)) \<Longrightarrow> f = g"
   apply (simp add: eq_iff)
   apply (blast intro: po_abstractn)
   done
 
 lemmas caseBs = caseBtrue caseBfalse caseBpair caseBlam caseBbot
 
 
 subsection \<open>Termination and Divergence\<close>
 
 lemma Trm_iff: "Trm(t) \<longleftrightarrow> \<not> t = bot"
   by (simp add: Trm_def Dvg_def)
 
 lemma Dvg_iff: "Dvg(t) \<longleftrightarrow> t = bot"
   by (simp add: Trm_def Dvg_def)
 
 
 subsection \<open>Constructors are injective\<close>
 
 lemma eq_lemma: "\<lbrakk>x=a; y=b; x=y\<rbrakk> \<Longrightarrow> a=b"
   by simp
 
 ML \<open>
   fun inj_rl_tac ctxt rews i =
     let
       fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
       val inj_lemmas = maps mk_inj_lemmas rews
     in
       CHANGED (REPEAT (assume_tac ctxt i ORELSE
         resolve_tac ctxt @{thms iffI allI conjI} i ORELSE
         eresolve_tac ctxt inj_lemmas i ORELSE
         asm_simp_tac (ctxt addsimps rews) i))
     end;
 \<close>
 
 method_setup inj_rl = \<open>
   Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
 \<close>
 
 lemma ccl_injs:
   "<a,b> = <a',b'> \<longleftrightarrow> (a=a' \<and> b=b')"
   "\<And>b b'. (lam x. b(x) = lam x. b'(x)) \<longleftrightarrow> ((ALL z. b(z)=b'(z)))"
   by (inj_rl caseBs)
 
 
 lemma pair_inject: "<a,b> = <a',b'> \<Longrightarrow> (a = a' \<Longrightarrow> b = b' \<Longrightarrow> R) \<Longrightarrow> R"
   by (simp add: ccl_injs)
 
 
 subsection \<open>Constructors are distinct\<close>
 
 lemma lem: "t=t' \<Longrightarrow> case(t,b,c,d,e) = case(t',b,c,d,e)"
   by simp
 
 ML \<open>
 local
-  fun pairs_of f x [] = []
+  fun pairs_of _ _ [] = []
     | pairs_of f x (y::ys) = (f x y) :: (f y x) :: (pairs_of f x ys)
 
-  fun mk_combs ff [] = []
+  fun mk_combs _ [] = []
     | mk_combs ff (x::xs) = (pairs_of ff x xs) @ mk_combs ff xs
 
   (* Doesn't handle binder types correctly *)
   fun saturate thy sy name =
-       let fun arg_str 0 a s = s
+       let fun arg_str 0 _ s = s
          | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
          | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
            val T = Sign.the_const_type thy (Sign.intern_const thy sy);
            val arity = length (binder_types T)
        in sy ^ (arg_str arity name "") end
 
   fun mk_thm_str thy a b = "\<not> " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
 
   val lemma = @{thm lem};
   val eq_lemma = @{thm eq_lemma};
   val distinctness = @{thm distinctness};
   fun mk_lemma (ra,rb) =
     [lemma] RL [ra RS (rb RS eq_lemma)] RL
     [distinctness RS @{thm notE}, @{thm sym} RS (distinctness RS @{thm notE})]
 in
   fun mk_lemmas rls = maps mk_lemma (mk_combs pair rls)
   fun mk_dstnct_rls thy xs = mk_combs (mk_thm_str thy) xs
 end
 \<close>
 
 ML \<open>
 val caseB_lemmas = mk_lemmas @{thms caseBs}
 
 val ccl_dstncts =
   let
     fun mk_raw_dstnct_thm rls s =
       Goal.prove_global \<^theory> [] [] (Syntax.read_prop_global \<^theory> s)
         (fn {context = ctxt, ...} => resolve_tac ctxt @{thms notI} 1 THEN eresolve_tac ctxt rls 1)
   in map (mk_raw_dstnct_thm caseB_lemmas)
     (mk_dstnct_rls \<^theory> ["bot","true","false","pair","lambda"]) end
 
 fun mk_dstnct_thms ctxt defs inj_rls xs =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun mk_dstnct_thm rls s =
       Goal.prove_global thy [] [] (Syntax.read_prop ctxt s)
         (fn _ =>
           rewrite_goals_tac ctxt defs THEN
           simp_tac (ctxt addsimps (rls @ inj_rls)) 1)
   in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
 
 fun mkall_dstnct_thms ctxt defs i_rls xss = maps (mk_dstnct_thms ctxt defs i_rls) xss
 
 (*** Rewriting and Proving ***)
 
 fun XH_to_I rl = rl RS @{thm iffD2}
 fun XH_to_D rl = rl RS @{thm iffD1}
 val XH_to_E = make_elim o XH_to_D
 val XH_to_Is = map XH_to_I
 val XH_to_Ds = map XH_to_D
 val XH_to_Es = map XH_to_E;
 
 ML_Thms.bind_thms ("ccl_rews", @{thms caseBs} @ @{thms ccl_injs} @ ccl_dstncts);
 ML_Thms.bind_thms ("ccl_dstnctsEs", ccl_dstncts RL [@{thm notE}]);
 ML_Thms.bind_thms ("ccl_injDs", XH_to_Ds @{thms ccl_injs});
 \<close>
 
 lemmas [simp] = ccl_rews
   and [elim!] = pair_inject ccl_dstnctsEs
   and [dest!] = ccl_injDs
 
 
 subsection \<open>Facts from gfp Definition of \<open>[=\<close> and \<open>=\<close>\<close>
 
 lemma XHlemma1: "\<lbrakk>A=B; a:B \<longleftrightarrow> P\<rbrakk> \<Longrightarrow> a:A \<longleftrightarrow> P"
   by simp
 
 lemma XHlemma2: "(P(t,t') \<longleftrightarrow> Q) \<Longrightarrow> (<t,t'> : {p. \<exists>t t'. p=<t,t'> \<and>  P(t,t')} \<longleftrightarrow> Q)"
   by blast
 
 
 subsection \<open>Pre-Order\<close>
 
 lemma POgen_mono: "mono(\<lambda>X. POgen(X))"
   apply (unfold POgen_def SIM_def)
   apply (rule monoI)
   apply blast
   done
 
 lemma POgenXH:
   "<t,t'> : POgen(R) \<longleftrightarrow> t= bot | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
            (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
            (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. <f(x),f'(x)> : R))"
   apply (unfold POgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma poXH:
   "t [= t' \<longleftrightarrow> t=bot | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
                  (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a [= a' \<and> b [= b') |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x) [= f'(x)))"
   apply (simp add: PO_iff del: ex_simps)
   apply (rule POgen_mono
     [THEN PO_def [THEN def_gfp_Tarski], THEN XHlemma1, unfolded POgen_def SIM_def])
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma po_bot: "bot [= b"
   apply (rule poXH [THEN iffD2])
   apply simp
   done
 
 lemma bot_poleast: "a [= bot \<Longrightarrow> a=bot"
   apply (drule poXH [THEN iffD1])
   apply simp
   done
 
 lemma po_pair: "<a,b> [= <a',b'> \<longleftrightarrow>  a [= a' \<and> b [= b'"
   apply (rule poXH [THEN iff_trans])
   apply simp
   done
 
 lemma po_lam: "lam x. f(x) [= lam x. f'(x) \<longleftrightarrow> (ALL x. f(x) [= f'(x))"
   apply (rule poXH [THEN iff_trans])
   apply fastforce
   done
 
 lemmas ccl_porews = po_bot po_pair po_lam
 
 lemma case_pocong:
   assumes 1: "t [= t'"
     and 2: "a [= a'"
     and 3: "b [= b'"
     and 4: "\<And>x y. c(x,y) [= c'(x,y)"
     and 5: "\<And>u. d(u) [= d'(u)"
   shows "case(t,a,b,c,d) [= case(t',a',b',c',d')"
   apply (rule 1 [THEN po_cong, THEN po_trans])
   apply (rule 2 [THEN po_cong, THEN po_trans])
   apply (rule 3 [THEN po_cong, THEN po_trans])
   apply (rule 4 [THEN po_abstractn, THEN po_abstractn, THEN po_cong, THEN po_trans])
   apply (rule_tac f1 = "\<lambda>d. case (t',a',b',c',d)" in
     5 [THEN po_abstractn, THEN po_cong, THEN po_trans])
   apply (rule po_refl)
   done
 
 lemma apply_pocong: "\<lbrakk>f [= f'; a [= a'\<rbrakk> \<Longrightarrow> f ` a [= f' ` a'"
   unfolding ccl_data_defs
   apply (rule case_pocong, (rule po_refl | assumption)+)
   apply (erule po_cong)
   done
 
 lemma npo_lam_bot: "\<not> lam x. b(x) [= bot"
   apply (rule notI)
   apply (drule bot_poleast)
   apply (erule distinctness [THEN notE])
   done
 
 lemma po_lemma: "\<lbrakk>x=a; y=b; x[=y\<rbrakk> \<Longrightarrow> a[=b"
   by simp
 
 lemma npo_pair_lam: "\<not> <a,b> [= lam x. f(x)"
   apply (rule notI)
   apply (rule npo_lam_bot [THEN notE])
   apply (erule case_pocong [THEN caseBlam [THEN caseBpair [THEN po_lemma]]])
   apply (rule po_refl npo_lam_bot)+
   done
 
 lemma npo_lam_pair: "\<not> lam x. f(x) [= <a,b>"
   apply (rule notI)
   apply (rule npo_lam_bot [THEN notE])
   apply (erule case_pocong [THEN caseBpair [THEN caseBlam [THEN po_lemma]]])
   apply (rule po_refl npo_lam_bot)+
   done
 
 lemma npo_rls1:
   "\<not> true [= false"
   "\<not> false [= true"
   "\<not> true [= <a,b>"
   "\<not> <a,b> [= true"
   "\<not> true [= lam x. f(x)"
   "\<not> lam x. f(x) [= true"
   "\<not> false [= <a,b>"
   "\<not> <a,b> [= false"
   "\<not> false [= lam x. f(x)"
   "\<not> lam x. f(x) [= false"
   by (rule notI, drule case_pocong, erule_tac [5] rev_mp, simp_all,
     (rule po_refl npo_lam_bot)+)+
 
 lemmas npo_rls = npo_pair_lam npo_lam_pair npo_rls1
 
 
 subsection \<open>Coinduction for \<open>[=\<close>\<close>
 
 lemma po_coinduct: "\<lbrakk><t,u> : R; R <= POgen(R)\<rbrakk> \<Longrightarrow> t [= u"
   apply (rule PO_def [THEN def_coinduct, THEN PO_iff [THEN iffD2]])
    apply assumption+
   done
 
 
 subsection \<open>Equality\<close>
 
 lemma EQgen_mono: "mono(\<lambda>X. EQgen(X))"
   apply (unfold EQgen_def SIM_def)
   apply (rule monoI)
   apply blast
   done
 
 lemma EQgenXH:
   "<t,t'> : EQgen(R) \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  |
                                              (t=false \<and> t'=false) |
                  (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> <a,a'> : R \<and> <b,b'> : R) |
                  (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x.<f(x),f'(x)> : R))"
   apply (unfold EQgen_def SIM_def)
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma eqXH:
   "t=t' \<longleftrightarrow> (t=bot \<and> t'=bot)  | (t=true \<and> t'=true)  | (t=false \<and> t'=false) |
                      (EX a a' b b'. t=<a,b> \<and> t'=<a',b'>  \<and> a=a' \<and> b=b') |
                      (EX f f'. t=lam x. f(x) \<and> t'=lam x. f'(x) \<and> (ALL x. f(x)=f'(x)))"
   apply (subgoal_tac "<t,t'> : EQ \<longleftrightarrow>
     (t=bot \<and> t'=bot) | (t=true \<and> t'=true) | (t=false \<and> t'=false) |
     (EX a a' b b'. t=<a,b> \<and> t'=<a',b'> \<and> <a,a'> : EQ \<and> <b,b'> : EQ) |
     (EX f f'. t=lam x. f (x) \<and> t'=lam x. f' (x) \<and> (ALL x. <f (x) ,f' (x) > : EQ))")
   apply (erule rev_mp)
   apply (simp add: EQ_iff [THEN iff_sym])
   apply (rule EQgen_mono [THEN EQ_def [THEN def_gfp_Tarski], THEN XHlemma1,
     unfolded EQgen_def SIM_def])
   apply (rule iff_refl [THEN XHlemma2])
   done
 
 lemma eq_coinduct: "\<lbrakk><t,u> : R; R <= EQgen(R)\<rbrakk> \<Longrightarrow> t = u"
   apply (rule EQ_def [THEN def_coinduct, THEN EQ_iff [THEN iffD2]])
    apply assumption+
   done
 
 lemma eq_coinduct3:
   "\<lbrakk><t,u> : R;  R <= EQgen(lfp(\<lambda>x. EQgen(x) Un R Un EQ))\<rbrakk> \<Longrightarrow> t = u"
   apply (rule EQ_def [THEN def_coinduct3, THEN EQ_iff [THEN iffD2]])
   apply (rule EQgen_mono | assumption)+
   done
 
 method_setup eq_coinduct3 = \<open>
   Scan.lift Args.embedded_inner_syntax >> (fn s => fn ctxt =>
     SIMPLE_METHOD'
       (Rule_Insts.res_inst_tac ctxt [((("R", 0), Position.none), s)] [] @{thm eq_coinduct3}))
 \<close>
 
 
 subsection \<open>Untyped Case Analysis and Other Facts\<close>
 
 lemma cond_eta: "(EX f. t=lam x. f(x)) \<Longrightarrow> t = lam x.(t ` x)"
   by (auto simp: apply_def)
 
 lemma exhaustion: "(t=bot) | (t=true) | (t=false) | (EX a b. t=<a,b>) | (EX f. t=lam x. f(x))"
   apply (cut_tac refl [THEN eqXH [THEN iffD1]])
   apply blast
   done
 
 lemma term_case:
   "\<lbrakk>P(bot); P(true); P(false); \<And>x y. P(<x,y>); \<And>b. P(lam x. b(x))\<rbrakk> \<Longrightarrow> P(t)"
   using exhaustion [of t] by blast
 
 end
diff --git a/src/CCL/Term.thy b/src/CCL/Term.thy
--- a/src/CCL/Term.thy
+++ b/src/CCL/Term.thy
@@ -1,319 +1,308 @@
 (*  Title:      CCL/Term.thy
     Author:     Martin Coen
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Definitions of usual program constructs in CCL\<close>
 
 theory Term
 imports CCL
 begin
 
 definition one :: "i"
   where "one == true"
 
 definition "if" :: "[i,i,i]\<Rightarrow>i"  ("(3if _/ then _/ else _)" [0,0,60] 60)
   where "if b then t else u  == case(b, t, u, \<lambda> x y. bot, \<lambda>v. bot)"
 
 definition inl :: "i\<Rightarrow>i"
   where "inl(a) == <true,a>"
 
 definition inr :: "i\<Rightarrow>i"
   where "inr(b) == <false,b>"
 
 definition split :: "[i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "split(t,f) == case(t, bot, bot, f, \<lambda>u. bot)"
 
 definition "when" :: "[i,i\<Rightarrow>i,i\<Rightarrow>i]\<Rightarrow>i"
   where "when(t,f,g) == split(t, \<lambda>b x. if b then f(x) else g(x))"
 
 definition fst :: "i\<Rightarrow>i"
   where "fst(t) == split(t, \<lambda>x y. x)"
 
 definition snd :: "i\<Rightarrow>i"
   where "snd(t) == split(t, \<lambda>x y. y)"
 
 definition thd :: "i\<Rightarrow>i"
   where "thd(t) == split(t, \<lambda>x p. split(p, \<lambda>y z. z))"
 
 definition zero :: "i"
   where "zero == inl(one)"
 
 definition succ :: "i\<Rightarrow>i"
   where "succ(n) == inr(n)"
 
 definition ncase :: "[i,i,i\<Rightarrow>i]\<Rightarrow>i"
   where "ncase(n,b,c) == when(n, \<lambda>x. b, \<lambda>y. c(y))"
 
-
-no_syntax
-  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
+  where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
 
-definition "let" :: "[i,i\<Rightarrow>i]\<Rightarrow>i"
-  where "let(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))"
-
-syntax
-  "_Let" :: "[letbinds, 'a] => 'a"  ("(let (_)/ in (_))" 10)
+syntax "_let1" :: "[idt,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
+translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)"
 
 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)"
 
 definition letrec2 :: "[[i,i,i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec2 (h, f) ==
     letrec (\<lambda>p g'. split(p,\<lambda>x y. h(x,y,\<lambda>u v. g'(<u,v>))), \<lambda>g'. f(\<lambda>x y. g'(<x,y>)))"
 
 definition letrec3 :: "[[i,i,i,i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i\<Rightarrow>i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i"
   where "letrec3 (h, f) ==
     letrec (\<lambda>p g'. split(p,\<lambda>x xs. split(xs,\<lambda>y z. h(x,y,z,\<lambda>u v w. g'(<u,<v,w>>)))),
       \<lambda>g'. f(\<lambda>x y z. g'(<x,<y,z>>)))"
 
 syntax
-  "_let" :: "[id,i,i]\<Rightarrow>i"  ("(3let _ be _/ in _)" [0,0,60] 60)
-  "_letrec" :: "[id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
-  "_letrec2" :: "[id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
-  "_letrec3" :: "[id,id,id,id,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
-
-ML \<open>
-(** Quantifier translations: variable binding **)
-
-(* FIXME does not handle "_idtdummy" *)
-(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *)
-
-fun let_tr [Free x, a, b] = Const(\<^const_syntax>\<open>let\<close>,dummyT) $ a $ absfree x b;
-fun let_tr' [a,Abs(id,T,b)] =
-     let val (id',b') = Syntax_Trans.variant_abs(id,T,b)
-     in Const(\<^syntax_const>\<open>_let\<close>,dummyT) $ Free(id',T) $ a $ b' end;
-
-fun letrec_tr [Free f, Free x, a, b] =
-      Const(\<^const_syntax>\<open>letrec\<close>, dummyT) $ absfree x (absfree f a) $ absfree f b;
-fun letrec2_tr [Free f, Free x, Free y, a, b] =
-      Const(\<^const_syntax>\<open>letrec2\<close>, dummyT) $ absfree x (absfree y (absfree f a)) $ absfree f b;
-fun letrec3_tr [Free f, Free x, Free y, Free z, a, b] =
-      Const(\<^const_syntax>\<open>letrec3\<close>, dummyT) $
-        absfree x (absfree y (absfree z (absfree f a))) $ absfree f b;
+  "_letrec" :: "[idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ be _/ in _)" [0,0,0,60] 60)
+  "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ be _/ in _)" [0,0,0,0,60] 60)
+  "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i"  ("(3letrec _ _ _ _ be _/ in _)" [0,0,0,0,0,60] 60)
+parse_translation \<open>
+  let
+    fun abs_tr t u = Syntax_Trans.abs_tr [t, u];
+    fun letrec_tr [f, x, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b;
+    fun letrec2_tr [f, x, y, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec2\<close> $ abs_tr x (abs_tr y (abs_tr f a)) $ abs_tr f b;
+    fun letrec3_tr [f, x, y, z, a, b] =
+      Syntax.const \<^const_syntax>\<open>letrec3\<close> $ abs_tr x (abs_tr y (abs_tr z (abs_tr f a))) $ abs_tr f b;
+  in
+    [(\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
+     (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
+     (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
+  end
+\<close>
+print_translation \<open>
+  let
+    val bound = Syntax_Trans.mark_bound_abs;
 
-fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val (_,a'') = Syntax_Trans.variant_abs(f,S,a)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a'')
-     in Const(\<^syntax_const>\<open>_letrec\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ a' $ b' end;
-fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
-         val (y',a2) = Syntax_Trans.variant_abs(y,U,a1)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a2)
-     in Const(\<^syntax_const>\<open>_letrec2\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ a' $ b'
+    fun letrec_tr' [Abs(x,T,Abs(f,S,a)),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val (_,a'') = Syntax_Trans.print_abs(f,S,a)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a'')
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec\<close> $ bound(f',SS) $ bound(x',T) $ a' $ b'
       end;
-fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
-     let val (f',b') = Syntax_Trans.variant_abs(ff,SS,b)
-         val ( _,a1) = Syntax_Trans.variant_abs(f,S,a)
-         val (z',a2) = Syntax_Trans.variant_abs(z,V,a1)
-         val (y',a3) = Syntax_Trans.variant_abs(y,U,a2)
-         val (x',a') = Syntax_Trans.variant_abs(x,T,a3)
-     in Const(\<^syntax_const>\<open>_letrec3\<close>,dummyT) $ Free(f',SS) $ Free(x',T) $ Free(y',U) $ Free(z',V) $ a' $ b'
-      end;
-\<close>
 
-parse_translation \<open>
- [(\<^syntax_const>\<open>_let\<close>, K let_tr),
-  (\<^syntax_const>\<open>_letrec\<close>, K letrec_tr),
-  (\<^syntax_const>\<open>_letrec2\<close>, K letrec2_tr),
-  (\<^syntax_const>\<open>_letrec3\<close>, K letrec3_tr)]
-\<close>
+    fun letrec2_tr' [Abs(x,T,Abs(y,U,Abs(f,S,a))),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (y',a2) = Syntax_Trans.print_abs(y,U,a1)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a2)
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec2\<close> $ bound(f',SS) $ bound(x',T) $ bound(y',U) $ a' $ b'
+      end;
 
-print_translation \<open>
- [(\<^const_syntax>\<open>let\<close>, K let_tr'),
-  (\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
-  (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
-  (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
+    fun letrec3_tr' [Abs(x,T,Abs(y,U,Abs(z,V,Abs(f,S,a)))),Abs(ff,SS,b)] =
+      let
+        val (f',b') = Syntax_Trans.print_abs(ff,SS,b)
+        val ( _,a1) = Syntax_Trans.print_abs(f,S,a)
+        val (z',a2) = Syntax_Trans.print_abs(z,V,a1)
+        val (y',a3) = Syntax_Trans.print_abs(y,U,a2)
+        val (x',a') = Syntax_Trans.print_abs(x,T,a3)
+      in
+        Syntax.const \<^syntax_const>\<open>_letrec3\<close> $
+          bound(f',SS) $ bound(x',T) $ bound(y',U) $ bound(z',V) $ a' $ b'
+      end;
+  in
+    [(\<^const_syntax>\<open>letrec\<close>, K letrec_tr'),
+     (\<^const_syntax>\<open>letrec2\<close>, K letrec2_tr'),
+     (\<^const_syntax>\<open>letrec3\<close>, K letrec3_tr')]
+  end
 \<close>
 
-
 definition nrec :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "nrec(n,b,c) == letrec g x be ncase(x, b, \<lambda>y. c(y,g(y))) in g(n)"
 
 definition nil :: "i"  ("([])")
   where "[] == inl(one)"
 
 definition cons :: "[i,i]\<Rightarrow>i"  (infixr "$" 80)
   where "h$t == inr(<h,t>)"
 
 definition lcase :: "[i,i,[i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lcase(l,b,c) == when(l, \<lambda>x. b, \<lambda>y. split(y,c))"
 
 definition lrec :: "[i,i,[i,i,i]\<Rightarrow>i]\<Rightarrow>i"
   where "lrec(l,b,c) == letrec g x be lcase(x, b, \<lambda>h t. c(h,t,g(t))) in g(l)"
 
 definition napply :: "[i\<Rightarrow>i,i,i]\<Rightarrow>i"  ("(_ ^ _ ` _)" [56,56,56] 56)
   where "f ^n` a == nrec(n,a,\<lambda>x g. f(g))"
 
 lemmas simp_can_defs = one_def inl_def inr_def
   and simp_ncan_defs = if_def when_def split_def fst_def snd_def thd_def
 lemmas simp_defs = simp_can_defs simp_ncan_defs
 
 lemmas ind_can_defs = zero_def succ_def nil_def cons_def
   and ind_ncan_defs = ncase_def nrec_def lcase_def lrec_def
 lemmas ind_defs = ind_can_defs ind_ncan_defs
 
 lemmas data_defs = simp_defs ind_defs napply_def
   and genrec_defs = letrec_def letrec2_def letrec3_def
 
 
 subsection \<open>Beta Rules, including strictness\<close>
 
 lemma letB: "\<not> t=bot \<Longrightarrow> let x be t in f(x) = f(t)"
   apply (unfold let_def)
   apply (erule rev_mp)
   apply (rule_tac t = "t" in term_case)
-      apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+      apply simp_all
   done
 
 lemma letBabot: "let x be bot in f(x) = bot"
-  apply (unfold let_def)
-  apply (rule caseBbot)
-  done
+  unfolding let_def by (rule caseBbot)
 
 lemma letBbbot: "let x be t in bot = bot"
   apply (unfold let_def)
   apply (rule_tac t = t in term_case)
       apply (rule caseBbot)
-     apply (simp_all add: caseBtrue caseBfalse caseBpair caseBlam)
+     apply simp_all
   done
 
 lemma applyB: "(lam x. b(x)) ` a = b(a)"
-  apply (unfold apply_def)
-  apply (simp add: caseBtrue caseBfalse caseBpair caseBlam)
-  done
+  by (simp add: apply_def)
 
 lemma applyBbot: "bot ` a = bot"
-  apply (unfold apply_def)
-  apply (rule caseBbot)
-  done
+  unfolding apply_def by (rule caseBbot)
 
 lemma fixB: "fix(f) = f(fix(f))"
   apply (unfold fix_def)
   apply (rule applyB [THEN ssubst], rule refl)
   done
 
-lemma letrecB:
-    "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
+lemma letrecB: "letrec g x be h(x,g) in g(a) = h(a,\<lambda>y. letrec g x be h(x,g) in g(y))"
   apply (unfold letrec_def)
   apply (rule fixB [THEN ssubst], rule applyB [THEN ssubst], rule refl)
   done
 
 lemmas rawBs = caseBs applyB applyBbot
 
 method_setup beta_rl = \<open>
   Scan.succeed (fn ctxt =>
-    SIMPLE_METHOD' (CHANGED o
-      simp_tac (ctxt addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB}))))
+    let val ctxt' = Context_Position.set_visible false ctxt in
+      SIMPLE_METHOD' (CHANGED o
+        simp_tac (ctxt' addsimps @{thms rawBs} setloop (fn _ => stac ctxt @{thm letrecB})))
+    end)
 \<close>
 
 lemma ifBtrue: "if true then t else u = t"
   and ifBfalse: "if false then t else u = u"
   and ifBbot: "if bot then t else u = bot"
   unfolding data_defs by beta_rl+
 
 lemma whenBinl: "when(inl(a),t,u) = t(a)"
   and whenBinr: "when(inr(a),t,u) = u(a)"
   and whenBbot: "when(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma splitB: "split(<a,b>,h) = h(a,b)"
   and splitBbot: "split(bot,h) = bot"
   unfolding data_defs by beta_rl+
 
 lemma fstB: "fst(<a,b>) = a"
   and fstBbot: "fst(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma sndB: "snd(<a,b>) = b"
   and sndBbot: "snd(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma thdB: "thd(<a,<b,c>>) = c"
   and thdBbot: "thd(bot) = bot"
   unfolding data_defs by beta_rl+
 
 lemma ncaseBzero: "ncase(zero,t,u) = t"
   and ncaseBsucc: "ncase(succ(n),t,u) = u(n)"
   and ncaseBbot: "ncase(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma nrecBzero: "nrec(zero,t,u) = t"
   and nrecBsucc: "nrec(succ(n),t,u) = u(n,nrec(n,t,u))"
   and nrecBbot: "nrec(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma lcaseBnil: "lcase([],t,u) = t"
   and lcaseBcons: "lcase(x$xs,t,u) = u(x,xs)"
   and lcaseBbot: "lcase(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma lrecBnil: "lrec([],t,u) = t"
   and lrecBcons: "lrec(x$xs,t,u) = u(x,xs,lrec(xs,t,u))"
   and lrecBbot: "lrec(bot,t,u) = bot"
   unfolding data_defs by beta_rl+
 
 lemma letrec2B:
   "letrec g x y be h(x,y,g) in g(p,q) = h(p,q,\<lambda>u v. letrec g x y be h(x,y,g) in g(u,v))"
   unfolding data_defs letrec2_def by beta_rl+
 
 lemma letrec3B:
   "letrec g x y z be h(x,y,z,g) in g(p,q,r) =
     h(p,q,r,\<lambda>u v w. letrec g x y z be h(x,y,z,g) in g(u,v,w))"
   unfolding data_defs letrec3_def by beta_rl+
 
 lemma napplyBzero: "f^zero`a = a"
   and napplyBsucc: "f^succ(n)`a = f(f^n`a)"
   unfolding data_defs by beta_rl+
 
 lemmas termBs = letB applyB applyBbot splitB splitBbot fstB fstBbot
   sndB sndBbot thdB thdBbot ifBtrue ifBfalse ifBbot whenBinl whenBinr
   whenBbot ncaseBzero ncaseBsucc ncaseBbot nrecBzero nrecBsucc
   nrecBbot lcaseBnil lcaseBcons lcaseBbot lrecBnil lrecBcons lrecBbot
   napplyBzero napplyBsucc
 
 
 subsection \<open>Constructors are injective\<close>
 
 lemma term_injs:
   "(inl(a) = inl(a')) \<longleftrightarrow> (a=a')"
   "(inr(a) = inr(a')) \<longleftrightarrow> (a=a')"
   "(succ(a) = succ(a')) \<longleftrightarrow> (a=a')"
   "(a$b = a'$b') \<longleftrightarrow> (a=a' \<and> b=b')"
   by (inj_rl applyB splitB whenBinl whenBinr ncaseBsucc lcaseBcons)
 
 
 subsection \<open>Constructors are distinct\<close>
 
 ML \<open>
 ML_Thms.bind_thms ("term_dstncts",
   mkall_dstnct_thms \<^context> @{thms data_defs} (@{thms ccl_injs} @ @{thms term_injs})
     [["bot","inl","inr"], ["bot","zero","succ"], ["bot","nil","cons"]]);
 \<close>
 
 
 subsection \<open>Rules for pre-order \<open>[=\<close>\<close>
 
 lemma term_porews:
   "inl(a) [= inl(a') \<longleftrightarrow> a [= a'"
   "inr(b) [= inr(b') \<longleftrightarrow> b [= b'"
   "succ(n) [= succ(n') \<longleftrightarrow> n [= n'"
   "x$xs [= x'$xs' \<longleftrightarrow> x [= x' \<and> xs [= xs'"
   by (simp_all add: data_defs ccl_porews)
 
 
 subsection \<open>Rewriting and Proving\<close>
 
 ML \<open>
   ML_Thms.bind_thms ("term_injDs", XH_to_Ds @{thms term_injs});
 \<close>
 
 lemmas term_rews = termBs term_injs term_dstncts ccl_porews term_porews
 
 lemmas [simp] = term_rews
 lemmas [elim!] = term_dstncts [THEN notE]
 lemmas [dest!] = term_injDs
 
 end
diff --git a/src/CCL/Trancl.thy b/src/CCL/Trancl.thy
--- a/src/CCL/Trancl.thy
+++ b/src/CCL/Trancl.thy
@@ -1,209 +1,206 @@
 (*  Title:      CCL/Trancl.thy
     Author:     Martin Coen, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 *)
 
 section \<open>Transitive closure of a relation\<close>
 
 theory Trancl
 imports CCL
 begin
 
 definition trans :: "i set \<Rightarrow> o"  (*transitivity predicate*)
   where "trans(r) == (ALL x y z. <x,y>:r \<longrightarrow> <y,z>:r \<longrightarrow> <x,z>:r)"
 
 definition id :: "i set"  (*the identity relation*)
   where "id == {p. EX x. p = <x,x>}"
 
 definition relcomp :: "[i set,i set] \<Rightarrow> i set"  (infixr "O" 60)  (*composition of relations*)
   where "r O s == {xz. EX x y z. xz = <x,z> \<and> <x,y>:s \<and> <y,z>:r}"
 
 definition rtrancl :: "i set \<Rightarrow> i set"  ("(_^*)" [100] 100)
   where "r^* == lfp(\<lambda>s. id Un (r O s))"
 
 definition trancl :: "i set \<Rightarrow> i set"  ("(_^+)" [100] 100)
   where "r^+ == r O rtrancl(r)"
 
 
 subsection \<open>Natural deduction for \<open>trans(r)\<close>\<close>
 
 lemma transI: "(\<And>x y z. \<lbrakk><x,y>:r; <y,z>:r\<rbrakk> \<Longrightarrow> <x,z>:r) \<Longrightarrow> trans(r)"
   unfolding trans_def by blast
 
 lemma transD: "\<lbrakk>trans(r); <a,b>:r; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c>:r"
   unfolding trans_def by blast
 
 
 subsection \<open>Identity relation\<close>
 
 lemma idI: "<a,a> : id"
   apply (unfold id_def)
   apply (rule CollectI)
   apply (rule exI)
   apply (rule refl)
   done
 
 lemma idE: "\<lbrakk>p: id;  \<And>x. p = <x,x> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (unfold id_def)
   apply (erule CollectE)
   apply blast
   done
 
 
 subsection \<open>Composition of two relations\<close>
 
 lemma compI: "\<lbrakk><a,b>:s; <b,c>:r\<rbrakk> \<Longrightarrow> <a,c> : r O s"
   unfolding relcomp_def by blast
 
 (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
 lemma compE: "\<lbrakk>xz : r O s; \<And>x y z. \<lbrakk>xz = <x,z>; <x,y>:s; <y,z>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   unfolding relcomp_def by blast
 
 lemma compEpair: "\<lbrakk><a,c> : r O s; \<And>y. \<lbrakk><a,y>:s; <y,c>:r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (erule compE)
   apply (simp add: pair_inject)
   done
 
 lemmas [intro] = compI idI
   and [elim] = compE idE
-  and [elim!] = pair_inject
 
 lemma comp_mono: "\<lbrakk>r'<=r; s'<=s\<rbrakk> \<Longrightarrow> (r' O s') <= (r O s)"
   by blast
 
 
 subsection \<open>The relation rtrancl\<close>
 
 lemma rtrancl_fun_mono: "mono(\<lambda>s. id Un (r O s))"
   apply (rule monoI)
   apply (rule monoI subset_refl comp_mono Un_mono)+
   apply assumption
   done
 
 lemma rtrancl_unfold: "r^* = id Un (r O r^*)"
   by (rule rtrancl_fun_mono [THEN rtrancl_def [THEN def_lfp_Tarski]])
 
 (*Reflexivity of rtrancl*)
 lemma rtrancl_refl: "<a,a> : r^*"
   apply (subst rtrancl_unfold)
   apply blast
   done
 
 (*Closure under composition with r*)
 lemma rtrancl_into_rtrancl: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^*"
   apply (subst rtrancl_unfold)
   apply blast
   done
 
 (*rtrancl of r contains r*)
 lemma r_into_rtrancl: "<a,b> : r \<Longrightarrow> <a,b> : r^*"
   apply (rule rtrancl_refl [THEN rtrancl_into_rtrancl])
   apply assumption
   done
 
 
 subsection \<open>standard induction rule\<close>
 
 lemma rtrancl_full_induct:
   "\<lbrakk><a,b> : r^*;
       \<And>x. P(<x,x>);
       \<And>x y z. \<lbrakk>P(<x,y>); <x,y>: r^*; <y,z>: r\<rbrakk>  \<Longrightarrow> P(<x,z>)\<rbrakk>
    \<Longrightarrow>  P(<a,b>)"
   apply (erule def_induct [OF rtrancl_def])
    apply (rule rtrancl_fun_mono)
   apply blast
   done
 
 (*nice induction rule*)
 lemma rtrancl_induct:
   "\<lbrakk><a,b> : r^*;
       P(a);
       \<And>y z. \<lbrakk><a,y> : r^*; <y,z> : r;  P(y)\<rbrakk> \<Longrightarrow> P(z) \<rbrakk>
     \<Longrightarrow> P(b)"
 (*by induction on this formula*)
   apply (subgoal_tac "ALL y. <a,b> = <a,y> \<longrightarrow> P(y)")
 (*now solve first subgoal: this formula is sufficient*)
   apply blast
 (*now do the induction*)
   apply (erule rtrancl_full_induct)
    apply blast
   apply blast
   done
 
 (*transitivity of transitive closure!! -- by induction.*)
 lemma trans_rtrancl: "trans(r^*)"
   apply (rule transI)
   apply (rule_tac b = z in rtrancl_induct)
     apply (fast elim: rtrancl_into_rtrancl)+
   done
 
 (*elimination of rtrancl -- by induction on a special formula*)
 lemma rtranclE:
   "\<lbrakk><a,b> : r^*; a = b \<Longrightarrow> P; \<And>y. \<lbrakk><a,y> : r^*; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (subgoal_tac "a = b | (EX y. <a,y> : r^* \<and> <y,b> : r)")
    prefer 2
    apply (erule rtrancl_induct)
     apply blast
    apply blast
   apply blast
   done
 
 
 subsection \<open>The relation trancl\<close>
 
 subsubsection \<open>Conversions between trancl and rtrancl\<close>
 
 lemma trancl_into_rtrancl: "<a,b> : r^+ \<Longrightarrow> <a,b> : r^*"
   apply (unfold trancl_def)
   apply (erule compEpair)
   apply (erule rtrancl_into_rtrancl)
   apply assumption
   done
 
 (*r^+ contains r*)
 lemma r_into_trancl: "<a,b> : r \<Longrightarrow> <a,b> : r^+"
   unfolding trancl_def by (blast intro: rtrancl_refl)
 
 (*intro rule by definition: from rtrancl and r*)
 lemma rtrancl_into_trancl1: "\<lbrakk><a,b> : r^*; <b,c> : r\<rbrakk> \<Longrightarrow> <a,c> : r^+"
   unfolding trancl_def by blast
 
 (*intro rule from r and rtrancl*)
 lemma rtrancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^*\<rbrakk> \<Longrightarrow> <a,c> : r^+"
   apply (erule rtranclE)
    apply (erule subst)
    apply (erule r_into_trancl)
   apply (rule trans_rtrancl [THEN transD, THEN rtrancl_into_trancl1])
     apply (assumption | rule r_into_rtrancl)+
   done
 
 (*elimination of r^+ -- NOT an induction rule*)
 lemma tranclE:
   "\<lbrakk><a,b> : r^+;
     <a,b> : r \<Longrightarrow> P;
     \<And>y. \<lbrakk><a,y> : r^+; <y,b> : r\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
   apply (subgoal_tac "<a,b> : r | (EX y. <a,y> : r^+ \<and> <y,b> : r)")
    apply blast
   apply (unfold trancl_def)
   apply (erule compEpair)
   apply (erule rtranclE)
    apply blast
   apply (blast intro!: rtrancl_into_trancl1)
   done
 
 (*Transitivity of r^+.
   Proved by unfolding since it uses transitivity of rtrancl. *)
 lemma trans_trancl: "trans(r^+)"
   apply (unfold trancl_def)
   apply (rule transI)
   apply (erule compEpair)+
   apply (erule rtrancl_into_rtrancl [THEN trans_rtrancl [THEN transD, THEN compI]])
     apply assumption+
   done
 
 lemma trancl_into_trancl2: "\<lbrakk><a,b> : r; <b,c> : r^+\<rbrakk> \<Longrightarrow> <a,c> : r^+"
-  apply (rule r_into_trancl [THEN trans_trancl [THEN transD]])
-   apply assumption+
-  done
+  by (rule r_into_trancl [THEN trans_trancl [THEN transD]])
 
 end
diff --git a/src/Pure/Syntax/syntax_trans.ML b/src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML
+++ b/src/Pure/Syntax/syntax_trans.ML
@@ -1,505 +1,498 @@
 (*  Title:      Pure/Syntax/syntax_trans.ML
     Author:     Tobias Nipkow and Markus Wenzel, TU Muenchen
 
 Syntax translation functions.
 *)
 
 signature BASIC_SYNTAX_TRANS =
 sig
   val eta_contract: bool Config.T
 end
 
 signature SYNTAX_TRANS =
 sig
   include BASIC_SYNTAX_TRANS
   val bracketsN: string
   val no_bracketsN: string
   val no_brackets: unit -> bool
   val type_bracketsN: string
   val no_type_bracketsN: string
   val no_type_brackets: unit -> bool
   val abs_tr: term list -> term
   val mk_binder_tr: string * string -> string * (Proof.context -> term list -> term)
   val antiquote_tr: string -> term -> term
   val quote_tr: string -> term -> term
   val quote_antiquote_tr: string -> string -> string ->
     string * (Proof.context -> term list -> term)
   val non_typed_tr': (Proof.context -> term list -> term) ->
     Proof.context -> typ -> term list -> term
   val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
   val mark_bound_abs: string * typ -> term
   val mark_bound_body: string * typ -> term
   val bound_vars: (string * typ) list -> term -> term
   val abs_tr': Proof.context -> term -> term
   val atomic_abs_tr': string * typ * term -> term * term
   val const_abs_tr': term -> term
   val mk_binder_tr': string * string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs_tr': string -> string -> string * (Proof.context -> term list -> term)
   val preserve_binder_abs2_tr': string -> string -> string * (Proof.context -> term list -> term)
-  val variant_abs: string * typ * term -> string * term
-  val variant_abs': string * typ * term -> string * term
+  val print_abs: string * typ * term -> string * term
   val dependent_tr': string * string -> term list -> term
   val antiquote_tr': string -> term -> term
   val quote_tr': string -> term -> term
   val quote_antiquote_tr': string -> string -> string ->
     string * (Proof.context -> term list -> term)
   val update_name_tr': term -> term
   val get_idents: Proof.context -> {structs: string list, fixes: string list}
   val put_idents: {structs: string list, fixes: string list} -> Proof.context -> Proof.context
   val pure_parse_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
   val pure_parse_translation: (string * (Proof.context -> term list -> term)) list
   val pure_print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list
 end;
 
 structure Syntax_Trans: SYNTAX_TRANS =
 struct
 
 structure Syntax = Lexicon.Syntax;
 
 
 (* print mode *)
 
 val bracketsN = "brackets";
 val no_bracketsN = "no_brackets";
 
 fun no_brackets () =
   find_first (fn mode => mode = bracketsN orelse mode = no_bracketsN)
     (print_mode_value ()) = SOME no_bracketsN;
 
 val type_bracketsN = "type_brackets";
 val no_type_bracketsN = "no_type_brackets";
 
 fun no_type_brackets () =
   find_first (fn mode => mode = type_bracketsN orelse mode = no_type_bracketsN)
     (print_mode_value ()) <> SOME type_bracketsN;
 
 
 
 (** parse (ast) translations **)
 
 (* strip_positions *)
 
 fun strip_positions_ast_tr [ast] = Ast.strip_positions ast
   | strip_positions_ast_tr asts = raise Ast.AST ("strip_positions_ast_tr", asts);
 
 
 (* constify *)
 
 fun constify_ast_tr [Ast.Appl [c as Ast.Constant "_constrain", ast1, ast2]] =
       Ast.Appl [c, constify_ast_tr [ast1], ast2]
   | constify_ast_tr [Ast.Variable c] = Ast.Constant c
   | constify_ast_tr asts = raise Ast.AST ("constify_ast_tr", asts);
 
 
 (* type syntax *)
 
 fun tapp_ast_tr [ty, c] = Ast.Appl [c, ty]
   | tapp_ast_tr asts = raise Ast.AST ("tapp_ast_tr", asts);
 
 fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
   | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
 
 fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
   | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
 
 
 (* application *)
 
 fun appl_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_args" args)
   | appl_ast_tr asts = raise Ast.AST ("appl_ast_tr", asts);
 
 fun applC_ast_tr [f, args] = Ast.Appl (f :: Ast.unfold_ast "_cargs" args)
   | applC_ast_tr asts = raise Ast.AST ("applC_ast_tr", asts);
 
 
 (* abstraction *)
 
 fun idtyp_ast_tr [x, ty] = Ast.Appl [Ast.Constant "_constrain", x, ty]
   | idtyp_ast_tr asts = raise Ast.AST ("idtyp_ast_tr", asts);
 
 fun lambda_ast_tr [pats, body] = Ast.fold_ast_p "_abs" (Ast.unfold_ast "_pttrns" pats, body)
   | lambda_ast_tr asts = raise Ast.AST ("lambda_ast_tr", asts);
 
 fun absfree_proper (x, T) t =
   if Name.is_internal x
   then error ("Illegal internal variable in abstraction: " ^ quote x)
   else absfree (x, T) t;
 
 fun abs_tr [Free x, t] = absfree_proper x t
   | abs_tr [Const ("_idtdummy", T), t] = absdummy T t
-  | abs_tr [Const ("_constrain", _) $ x $ tT, t] =
-      Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
+  | abs_tr [Const ("_constrain", _) $ x $ tT, t] = Syntax.const "_constrainAbs" $ abs_tr [x, t] $ tT
   | abs_tr ts = raise TERM ("abs_tr", ts);
 
 
 (* binder *)
 
 fun mk_binder_tr (syn, name) =
   let
     fun err ts = raise TERM ("binder_tr: " ^ syn, ts)
     fun binder_tr [Const ("_idts", _) $ idt $ idts, t] = binder_tr [idt, binder_tr [idts, t]]
-      | binder_tr [x, t] =
-          let val abs = abs_tr [x, t] handle TERM _ => err [x, t]
-          in Syntax.const name $ abs end
+      | binder_tr [x, t] = Syntax.const name $ (abs_tr [x, t] handle TERM _ => err [x, t])
       | binder_tr ts = err ts;
   in (syn, fn _ => binder_tr) end;
 
 
 (* type propositions *)
 
 fun mk_type ty =
   Syntax.const "_constrain" $
     Syntax.const "\<^const>Pure.type" $ (Syntax.const "\<^type>itself" $ ty);
 
 fun ofclass_tr [ty, cls] = cls $ mk_type ty
   | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
 
 fun sort_constraint_tr [ty] = Syntax.const "\<^const>Pure.sort_constraint" $ mk_type ty
   | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
 
 
 (* meta propositions *)
 
 fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\<^type>prop"
   | aprop_tr ts = raise TERM ("aprop_tr", ts);
 
 
 (* meta implication *)
 
 fun bigimpl_ast_tr (asts as [asms, concl]) =
       let val prems =
         (case Ast.unfold_ast_p "_asms" asms of
           (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
         | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
       in Ast.fold_ast_p "\<^const>Pure.imp" (prems, concl) end
   | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
 
 
 (* type/term reflection *)
 
 fun type_tr [ty] = mk_type ty
   | type_tr ts = raise TERM ("type_tr", ts);
 
 
 (* quote / antiquote *)
 
 fun antiquote_tr name =
   let
     fun tr i ((t as Const (c, _)) $ u) =
           if c = name then tr i u $ Bound i
           else tr i t $ tr i u
       | tr i (t $ u) = tr i t $ tr i u
       | tr i (Abs (x, T, t)) = Abs (x, T, tr (i + 1) t)
       | tr _ a = a;
   in tr 0 end;
 
 fun quote_tr name t = Abs ("s", dummyT, antiquote_tr name (Term.incr_boundvars 1 t));
 
 fun quote_antiquote_tr quoteN antiquoteN name =
   let
     fun tr [t] = Syntax.const name $ quote_tr antiquoteN t
       | tr ts = raise TERM ("quote_tr", ts);
   in (quoteN, fn _ => tr) end;
 
 
 (* corresponding updates *)
 
 fun update_name_tr (Free (x, T) :: ts) = list_comb (Free (suffix "_update" x, T), ts)
   | update_name_tr (Const (x, T) :: ts) = list_comb (Const (suffix "_update" x, T), ts)
   | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
       if Term_Position.is_position ty then list_comb (c $ update_name_tr [t] $ ty, ts)
       else
         list_comb (c $ update_name_tr [t] $
           (Lexicon.fun_type $
             (Lexicon.fun_type $ Lexicon.dummy_type $ ty) $ Lexicon.dummy_type), ts)
   | update_name_tr ts = raise TERM ("update_name_tr", ts);
 
 
 (* indexed syntax *)
 
 structure Idents = Proof_Data
 (
   type T = {structs: string list, fixes: string list};
   fun init _ : T = {structs = [], fixes = []};
 );
 
 val get_idents = Idents.get;
 val put_idents = Idents.put;
 
 fun indexdefault_ast_tr [] =
       Ast.Appl [Ast.Constant "_index",
         Ast.Appl [Ast.Constant "_struct", Ast.Constant "_indexdefault"]]
   | indexdefault_ast_tr asts = raise Ast.AST ("indexdefault_ast_tr", asts);
 
 fun indexvar_ast_tr [] = Ast.Appl [Ast.Constant "_index", Ast.Variable "some_index"]
   | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
 
 fun struct_ast_tr [Ast.Appl [Ast.Constant "_index", ast]] = ast
   | struct_ast_tr asts = Ast.mk_appl (Ast.Constant "_struct") asts;
 
 fun index_tr [t] = t
   | index_tr ts = raise TERM ("index_tr", ts);
 
 fun struct_tr ctxt [Const ("_indexdefault", _)] =
       (case #structs (get_idents ctxt) of
         x :: _ => Syntax.const (Lexicon.mark_fixed x)
       | _ => error "Illegal reference to implicit structure")
   | struct_tr _ ts = raise TERM ("struct_tr", ts);
 
 
 
 (** print (ast) translations **)
 
 (* types *)
 
 fun non_typed_tr' f ctxt _ ts = f ctxt ts;
 
 
 (* type syntax *)
 
 fun tappl_ast_tr' (f, []) = raise Ast.AST ("tappl_ast_tr'", [f])
   | tappl_ast_tr' (f, [ty]) = Ast.Appl [Ast.Constant "_tapp", ty, f]
   | tappl_ast_tr' (f, ty :: tys) =
       Ast.Appl [Ast.Constant "_tappl", ty, Ast.fold_ast "_types" tys, f];
 
 fun fun_ast_tr' asts =
   if no_brackets () orelse no_type_brackets () then raise Match
   else
     (case Ast.unfold_ast_p "\<^type>fun" (Ast.Appl (Ast.Constant "\<^type>fun" :: asts)) of
       (dom as _ :: _ :: _, cod)
         => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
     | _ => raise Match);
 
 
 (* application *)
 
 fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])
   | appl_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_appl", f, Ast.fold_ast "_args" args];
 
 fun applC_ast_tr' (f, []) = raise Ast.AST ("applC_ast_tr'", [f])
   | applC_ast_tr' (f, args) = Ast.Appl [Ast.Constant "_applC", f, Ast.fold_ast "_cargs" args];
 
 
 (* partial eta-contraction before printing *)
 
 fun eta_abs (Abs (a, T, t)) =
       (case eta_abs t of
         t' as Const ("_aprop", _) $ _ => Abs (a, T, t')
       | t' as f $ u =>
           (case eta_abs u of
             Bound 0 =>
               if Term.is_dependent f then Abs (a, T, t')
               else incr_boundvars ~1 f
           | _ => Abs (a, T, t'))
       | t' => Abs (a, T, t'))
   | eta_abs t = t;
 
 val eta_contract = Config.declare_option_bool ("eta_contract", \<^here>);
 fun eta_contr ctxt = Config.get ctxt eta_contract ? eta_abs;
 
 
 (* abstraction *)
 
 fun mark_bound_abs (x, T) = Const ("_bound", T --> T) $ Free (x, T);
 fun mark_bound_body (x, T) = Const ("_bound", dummyT) $ Free (x, T);
 
 fun bound_vars vars body =
   subst_bounds (map mark_bound_abs (Term.rename_wrt_term body vars), body);
 
 fun strip_abss vars_of body_of tm =
   let
     val vars = vars_of tm;
     val body = body_of tm;
     val rev_new_vars = Term.rename_wrt_term body vars;
     fun subst (x, T) b =
       if Name.is_internal x andalso not (Term.is_dependent b)
       then (Const ("_idtdummy", T), incr_boundvars ~1 b)
       else (mark_bound_abs (x, T), Term.subst_bound (mark_bound_body (x, T), b));
     val (rev_vars', body') = fold_map subst rev_new_vars body;
   in (rev rev_vars', body') end;
 
 
 fun abs_tr' ctxt tm =
   uncurry (fold_rev (fn x => fn t => Syntax.const "_abs" $ x $ t))
     (strip_abss strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
 fun atomic_abs_tr' (x, T, t) =
   let val [xT] = Term.rename_wrt_term t [(x, T)]
   in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
     ([], _) => raise Ast.AST ("abs_ast_tr'", asts)
   | (xs, body) => Ast.Appl [Ast.Constant "_lambda", Ast.fold_ast "_pttrns" xs, body]);
 
 fun const_abs_tr' t =
   (case eta_abs t of
     Abs (_, _, t') =>
       if Term.is_dependent t' then raise Match
       else incr_boundvars ~1 t'
   | _ => raise Match);
 
 
 (* binders *)
 
 fun mk_binder_tr' (name, syn) =
   let
     fun mk_idts [] = raise Match    (*abort translation*)
       | mk_idts [idt] = idt
       | mk_idts (idt :: idts) = Syntax.const "_idts" $ idt $ mk_idts idts;
 
     fun tr' t =
       let
         val (xs, bd) = strip_abss (strip_qnt_vars name) (strip_qnt_body name) t;
       in Syntax.const syn $ mk_idts xs $ bd end;
 
     fun binder_tr' (t :: ts) = Term.list_comb (tr' (Syntax.const name $ t), ts)
       | binder_tr' [] = raise Match;
   in (name, fn _ => binder_tr') end;
 
 fun preserve_binder_abs_tr' name syn = (name, fn _ => fn Abs abs :: ts =>
   let val (x, t) = atomic_abs_tr' abs
   in list_comb (Syntax.const syn $ x $ t, ts) end);
 
 fun preserve_binder_abs2_tr' name syn = (name, fn _ => fn A :: Abs abs :: ts =>
   let val (x, t) = atomic_abs_tr' abs
   in list_comb (Syntax.const syn $ x $ A $ t, ts) end);
 
 
 (* idtyp constraints *)
 
 fun idtyp_ast_tr' a [Ast.Appl [Ast.Constant "_constrain", x, ty], xs] =
       Ast.Appl [Ast.Constant a, Ast.Appl [Ast.Constant "_idtyp", x, ty], xs]
   | idtyp_ast_tr' _ _ = raise Match;
 
 
 (* meta implication *)
 
 fun impl_ast_tr' asts =
   if no_brackets () then raise Match
   else
     (case Ast.unfold_ast_p "\<^const>Pure.imp"
         (Ast.Appl (Ast.Constant "\<^const>Pure.imp" :: asts)) of
       (prems as _ :: _ :: _, concl) =>
         let
           val (asms, asm) = split_last prems;
           val asms' = Ast.fold_ast_p "_asms" (asms, Ast.Appl [Ast.Constant "_asm", asm]);
         in Ast.Appl [Ast.Constant "_bigimpl", asms', concl] end
     | _ => raise Match);
 
 
 (* dependent / nondependent quantifiers *)
 
-fun var_abs mark (x, T, b) =
+fun print_abs (x, T, b) =
   let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
-  in (x', subst_bound (mark (x', T), b)) end;
-
-val variant_abs = var_abs Free;
-val variant_abs' = var_abs mark_bound_abs;
+  in (x', subst_bound (mark_bound_abs (x', T), b)) end;
 
 fun dependent_tr' (q, r) (A :: Abs (x, T, B) :: ts) =
       if Term.is_dependent B then
-        let val (x', B') = variant_abs' (x, dummyT, B);
+        let val (x', B') = print_abs (x, dummyT, B);
         in Term.list_comb (Syntax.const q $ mark_bound_abs (x', T) $ A $ B', ts) end
       else Term.list_comb (Syntax.const r $ A $ incr_boundvars ~1 B, ts)
   | dependent_tr' _ _ = raise Match;
 
 
 (* quote / antiquote *)
 
 fun antiquote_tr' name =
   let
     fun tr' i (t $ u) =
           if u aconv Bound i then Syntax.const name $ tr' i t
           else tr' i t $ tr' i u
       | tr' i (Abs (x, T, t)) = Abs (x, T, tr' (i + 1) t)
       | tr' i a = if a aconv Bound i then raise Match else a;
   in tr' 0 end;
 
 fun quote_tr' name (Abs (_, _, t)) = Term.incr_boundvars ~1 (antiquote_tr' name t)
   | quote_tr' _ _ = raise Match;
 
 fun quote_antiquote_tr' quoteN antiquoteN name =
   let
     fun tr' (t :: ts) = Term.list_comb (Syntax.const quoteN $ quote_tr' antiquoteN t, ts)
       | tr' _ = raise Match;
   in (name, fn _ => tr') end;
 
 
 (* corresponding updates *)
 
 local
 
 fun upd_type (Type ("fun", [Type ("fun", [_, T]), _])) = T
   | upd_type _ = dummyT;
 
 fun upd_tr' (x_upd, T) =
   (case try (unsuffix "_update") x_upd of
     SOME x => (x, upd_type T)
   | NONE => raise Match);
 
 in
 
 fun update_name_tr' (Free x) = Free (upd_tr' x)
   | update_name_tr' ((c as Const ("_free", _)) $ Free x) = c $ Free (upd_tr' x)
   | update_name_tr' (Const x) = Const (upd_tr' x)
   | update_name_tr' _ = raise Match;
 
 end;
 
 
 (* indexed syntax *)
 
 fun index_ast_tr' [Ast.Appl [Ast.Constant "_struct", ast]] = ast
   | index_ast_tr' _ = raise Match;
 
 fun struct_ast_tr' ctxt [Ast.Constant "_indexdefault"] =
       (case #structs (get_idents ctxt) of
         x :: _ => Ast.Appl [Ast.Constant "_free", Ast.Variable x]
       | _ => raise Match)
   | struct_ast_tr' _ _ = raise Match;
 
 
 
 (** Pure translations **)
 
 val pure_parse_ast_translation =
  [("_strip_positions", fn _ => strip_positions_ast_tr),
   ("_constify", fn _ => constify_ast_tr),
   ("_tapp", fn _ => tapp_ast_tr),
   ("_tappl", fn _ => tappl_ast_tr),
   ("_bracket", fn _ => bracket_ast_tr),
   ("_appl", fn _ => appl_ast_tr),
   ("_applC", fn _ => applC_ast_tr),
   ("_lambda", fn _ => lambda_ast_tr),
   ("_idtyp", fn _ => idtyp_ast_tr),
   ("_bigimpl", fn _ => bigimpl_ast_tr),
   ("_indexdefault", fn _ => indexdefault_ast_tr),
   ("_indexvar", fn _ => indexvar_ast_tr),
   ("_struct", fn _ => struct_ast_tr)];
 
 val pure_parse_translation =
  [("_abs", fn _ => abs_tr),
   ("_aprop", fn _ => aprop_tr),
   ("_ofclass", fn _ => ofclass_tr),
   ("_sort_constraint", fn _ => sort_constraint_tr),
   ("_TYPE", fn _ => type_tr),
   ("_update_name", fn _ => update_name_tr),
   ("_index", fn _ => index_tr),
   ("_struct", struct_tr)];
 
 val pure_print_ast_translation =
  [("\<^type>fun", fn _ => fun_ast_tr'),
   ("_abs", fn _ => abs_ast_tr'),
   ("_idts", fn _ => idtyp_ast_tr' "_idts"),
   ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
   ("\<^const>Pure.imp", fn _ => impl_ast_tr'),
   ("_index", fn _ => index_ast_tr'),
   ("_struct", struct_ast_tr')];
 
 end;
 
 structure Basic_Syntax_Trans: BASIC_SYNTAX_TRANS = Syntax_Trans;
 open Basic_Syntax_Trans;
diff --git a/src/Pure/Tools/build_docker.scala b/src/Pure/Tools/build_docker.scala
--- a/src/Pure/Tools/build_docker.scala
+++ b/src/Pure/Tools/build_docker.scala
@@ -1,160 +1,160 @@
 /*  Title:      Pure/Tools/build_docker.scala
     Author:     Makarius
 
 Build docker image from Isabelle application bundle for Linux.
 */
 
 package isabelle
 
 
 object Build_Docker
 {
   private val default_base = "ubuntu"
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
 
   private val Isabelle_Name = """^.*?(Isabelle[^/\\:]+)_linux\.tar\.gz$""".r
 
   val packages: List[String] =
-    List("curl", "less", "libfontconfig1", "libgomp1", "perl", "pwgen", "rlwrap", "unzip")
+    List("curl", "less", "libfontconfig1", "libgomp1", "pwgen", "rlwrap", "unzip")
 
   val package_collections: Map[String, List[String]] =
     Map("X11" -> List("libx11-6", "libxext6", "libxrender1", "libxtst6", "libxi6"),
       "latex" ->
         List("texlive-fonts-extra", "texlive-font-utils", "texlive-latex-extra", "texlive-science"))
 
   def build_docker(progress: Progress,
     app_archive: String,
     base: String = default_base,
     logic: String = default_logic,
     no_build: Boolean = false,
     entrypoint: Boolean = false,
     output: Option[Path] = None,
     more_packages: List[String] = Nil,
     tag: String = "",
     verbose: Boolean = false): Unit =
   {
     val isabelle_name =
       app_archive match {
         case Isabelle_Name(name) => name
         case _ => error("Cannot determine Isabelle distribution name from " + app_archive)
       }
     val is_remote = Url.is_wellformed(app_archive)
 
     val dockerfile =
       """## Dockerfile for """ + isabelle_name + """
 
 FROM """ + base + """
 SHELL ["/bin/bash", "-c"]
 
 # packages
 ENV DEBIAN_FRONTEND=noninteractive
 RUN apt-get -y update && \
   apt-get install -y """ + Bash.strings(packages ::: more_packages) + """ && \
   apt-get clean
 
 # user
 RUN useradd -m isabelle && (echo isabelle:isabelle | chpasswd)
 USER isabelle
 
 # Isabelle
 WORKDIR /home/isabelle
 """ +
  (if (is_remote)
    "RUN curl --fail --silent " + Bash.string(app_archive) + " > Isabelle.tar.gz"
   else "COPY Isabelle.tar.gz .") +
 """
 RUN tar xzf Isabelle.tar.gz && \
   mv """ + isabelle_name + """ Isabelle && \
   perl -pi -e 's,ISABELLE_HOME_USER=.*,ISABELLE_HOME_USER="\$USER_HOME/.isabelle",g;' Isabelle/etc/settings && \
   perl -pi -e 's,ISABELLE_LOGIC=.*,ISABELLE_LOGIC=""" + logic + """,g;' Isabelle/etc/settings && \
   Isabelle/bin/isabelle build -o system_heaps -b """ + logic + """ && \
   rm Isabelle.tar.gz""" +
  (if (entrypoint) """
 
 ENTRYPOINT ["Isabelle/bin/isabelle"]
 """
   else "")
 
     output.foreach(File.write(_, dockerfile))
 
     if (!no_build) {
       Isabelle_System.with_tmp_dir("docker")(tmp_dir =>
         {
           File.write(tmp_dir + Path.explode("Dockerfile"), dockerfile)
 
           if (is_remote) {
             if (!Url.is_readable(app_archive))
               error("Cannot access remote archive " + app_archive)
           }
           else Isabelle_System.copy_file(Path.explode(app_archive),
             tmp_dir + Path.explode("Isabelle.tar.gz"))
 
           val quiet_option = if (verbose) "" else " -q"
           val tag_option = if (tag == "") "" else " -t " + Bash.string(tag)
           progress.bash("docker build" + quiet_option + tag_option + " " + File.bash_path(tmp_dir),
             echo = true).check
         })
     }
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_docker", "build Isabelle docker image",
       Scala_Project.here, args =>
     {
       var base = default_base
       var entrypoint = false
       var logic = default_logic
       var no_build = false
       var output: Option[Path] = None
       var more_packages: List[String] = Nil
       var verbose = false
       var tag = ""
 
       val getopts =
         Getopts("""
 Usage: isabelle build_docker [OPTIONS] APP_ARCHIVE
 
   Options are:
     -B NAME      base image (default """ + quote(default_base) + """)
     -E           set Isabelle/bin/isabelle as entrypoint
     -P NAME      additional Ubuntu package collection (""" +
           package_collections.keySet.toList.sorted.map(quote(_)).mkString(", ") + """)
     -l NAME      default logic (default ISABELLE_LOGIC=""" + quote(default_logic) + """)
     -n           no docker build
     -o FILE      output generated Dockerfile
     -p NAME      additional Ubuntu package
     -t TAG       docker build tag
     -v           verbose
 
   Build Isabelle docker image with default logic image, using a standard
   Isabelle application archive for Linux (local file or remote URL).
 """,
           "B:" -> (arg => base = arg),
           "E" -> (_ => entrypoint = true),
           "P:" -> (arg =>
             package_collections.get(arg) match {
               case Some(ps) => more_packages :::= ps
               case None => error("Unknown package collection " + quote(arg))
             }),
           "l:" -> (arg => logic = arg),
           "n" -> (_ => no_build = true),
           "o:" -> (arg => output = Some(Path.explode(arg))),
           "p:" -> (arg => more_packages ::= arg),
           "t:" -> (arg => tag = arg),
           "v" -> (_ => verbose = true))
 
       val more_args = getopts(args)
       val app_archive =
         more_args match {
           case List(arg) => arg
           case _ => getopts.usage()
         }
 
       build_docker(new Console_Progress(), app_archive, base = base, logic = logic,
         no_build = no_build, entrypoint = entrypoint, output = output,
         more_packages = more_packages, tag = tag, verbose = verbose)
     })
 }
diff --git a/src/Pure/term.ML b/src/Pure/term.ML
--- a/src/Pure/term.ML
+++ b/src/Pure/term.ML
@@ -1,1050 +1,1051 @@
 (*  Title:      Pure/term.ML
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Author:     Makarius
 
 Simply typed lambda-calculus: types, terms, and basic operations.
 *)
 
 infix 9 $;
 infixr 5 -->;
 infixr --->;
 infix aconv;
 
 signature BASIC_TERM =
 sig
   type indexname = string * int
   type class = string
   type sort = class list
   type arity = string * sort list * sort
   datatype typ =
     Type  of string * typ list |
     TFree of string * sort |
     TVar  of indexname * sort
   datatype term =
     Const of string * typ |
     Free of string * typ |
     Var of indexname * typ |
     Bound of int |
     Abs of string * typ * term |
     $ of term * term
   exception TYPE of string * typ list * term list
   exception TERM of string * term list
   val dummyS: sort
   val dummyT: typ
   val no_dummyT: typ -> typ
   val --> : typ * typ -> typ
   val ---> : typ list * typ -> typ
   val is_Type: typ -> bool
   val is_TFree: typ -> bool
   val is_TVar: typ -> bool
   val dest_Type: typ -> string * typ list
   val dest_TFree: typ -> string * sort
   val dest_TVar: typ -> indexname * sort
   val is_Bound: term -> bool
   val is_Const: term -> bool
   val is_Free: term -> bool
   val is_Var: term -> bool
   val dest_Const: term -> string * typ
   val dest_Free: term -> string * typ
   val dest_Var: term -> indexname * typ
   val dest_comb: term -> term * term
   val domain_type: typ -> typ
   val range_type: typ -> typ
   val dest_funT: typ -> typ * typ
   val binder_types: typ -> typ list
   val body_type: typ -> typ
   val strip_type: typ -> typ list * typ
   val type_of1: typ list * term -> typ
   val type_of: term -> typ
   val fastype_of1: typ list * term -> typ
   val fastype_of: term -> typ
   val strip_abs: term -> (string * typ) list * term
   val strip_abs_body: term -> term
   val strip_abs_vars: term -> (string * typ) list
   val strip_qnt_body: string -> term -> term
   val strip_qnt_vars: string -> term -> (string * typ) list
   val list_comb: term * term list -> term
   val strip_comb: term -> term * term list
   val head_of: term -> term
   val size_of_term: term -> int
   val size_of_typ: typ -> int
   val map_atyps: (typ -> typ) -> typ -> typ
   val map_aterms: (term -> term) -> term -> term
   val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
   val map_type_tfree: (string * sort -> typ) -> typ -> typ
   val map_types: (typ -> typ) -> term -> term
   val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
   val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
   val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
   val burrow_types: (typ list -> typ list) -> term list -> term list
   val aconv: term * term -> bool
   val propT: typ
   val strip_all_body: term -> term
   val strip_all_vars: term -> (string * typ) list
   val incr_bv: int * int * term -> term
   val incr_boundvars: int -> term -> term
   val add_loose_bnos: term * int * int list -> int list
   val loose_bnos: term -> int list
   val loose_bvar: term * int -> bool
   val loose_bvar1: term * int -> bool
   val subst_bounds: term list * term -> term
   val subst_bound: term * term -> term
   val betapply: term * term -> term
   val betapplys: term * term list -> term
   val subst_free: (term * term) list -> term -> term
   val abstract_over: term * term -> term
   val lambda: term -> term -> term
   val absfree: string * typ -> term -> term
   val absdummy: typ -> term -> term
   val subst_atomic: (term * term) list -> term -> term
   val typ_subst_atomic: (typ * typ) list -> typ -> typ
   val subst_atomic_types: (typ * typ) list -> term -> term
   val typ_subst_TVars: (indexname * typ) list -> typ -> typ
   val subst_TVars: (indexname * typ) list -> term -> term
   val subst_Vars: (indexname * term) list -> term -> term
   val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term
   val is_first_order: string list -> term -> bool
   val maxidx_of_typ: typ -> int
   val maxidx_of_typs: typ list -> int
   val maxidx_of_term: term -> int
   val fold_subtypes: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
   val exists_subtype: (typ -> bool) -> typ -> bool
   val exists_type: (typ -> bool) -> term -> bool
   val exists_subterm: (term -> bool) -> term -> bool
   val exists_Const: (string * typ -> bool) -> term -> bool
 end;
 
 signature TERM =
 sig
   include BASIC_TERM
   val aT: sort -> typ
   val itselfT: typ -> typ
   val a_itselfT: typ
   val argument_type_of: term -> int -> typ
   val abs: string * typ -> term -> term
   val add_tvar_namesT: typ -> indexname list -> indexname list
   val add_tvar_names: term -> indexname list -> indexname list
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
   val add_var_names: term -> indexname list -> indexname list
   val add_vars: term -> (indexname * typ) list -> (indexname * typ) list
   val add_tfree_namesT: typ -> string list -> string list
   val add_tfree_names: term -> string list -> string list
   val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   val add_free_names: term -> string list -> string list
   val add_frees: term -> (string * typ) list -> (string * typ) list
   val add_const_names: term -> string list -> string list
   val add_consts: term -> (string * typ) list -> (string * typ) list
   val hidden_polymorphism: term -> (indexname * sort) list
   val declare_typ_names: typ -> Name.context -> Name.context
   val declare_term_names: term -> Name.context -> Name.context
   val declare_term_frees: term -> Name.context -> Name.context
   val variant_frees: term -> (string * 'a) list -> (string * 'a) list
   val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
   val eq_ix: indexname * indexname -> bool
   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   val eq_var: (indexname * typ) * (indexname * typ) -> bool
   val aconv_untyped: term * term -> bool
   val could_unify: term * term -> bool
   val strip_abs_eta: int -> term -> (string * typ) list * term
   val match_bvars: (term * term) -> (string * string) list -> (string * string) list
   val map_abs_vars: (string -> string) -> term -> term
   val rename_abs: term -> term -> term -> term option
   val is_open: term -> bool
   val is_dependent: term -> bool
   val term_name: term -> string
   val dependent_lambda_name: string * term -> term -> term
   val lambda_name: string * term -> term -> term
   val close_schematic_term: term -> term
   val maxidx_typ: typ -> int -> int
   val maxidx_typs: typ list -> int -> int
   val maxidx_term: term -> int -> int
   val could_beta_contract: term -> bool
   val could_eta_contract: term -> bool
   val could_beta_eta_contract: term -> bool
+  val used_free: string -> term -> bool
   val dest_abs: string * typ * term -> string * term
   val dummy_pattern: typ -> term
   val dummy: term
   val dummy_prop: term
   val is_dummy_pattern: term -> bool
   val free_dummy_patterns: term -> Name.context -> term * Name.context
   val no_dummy_patterns: term -> term
   val replace_dummy_patterns: term -> int -> term * int
   val show_dummy_patterns: term -> term
   val string_of_vname: indexname -> string
   val string_of_vname': indexname -> string
 end;
 
 structure Term: TERM =
 struct
 
 (*Indexnames can be quickly renamed by adding an offset to the integer part,
   for resolution.*)
 type indexname = string * int;
 
 (*Types are classified by sorts.*)
 type class = string;
 type sort  = class list;
 type arity = string * sort list * sort;
 
 (*The sorts attached to TFrees and TVars specify the sort of that variable.*)
 datatype typ = Type  of string * typ list
              | TFree of string * sort
              | TVar  of indexname * sort;
 
 (*Terms.  Bound variables are indicated by depth number.
   Free variables, (scheme) variables and constants have names.
   An term is "closed" if every bound variable of level "lev"
   is enclosed by at least "lev" abstractions.
 
   It is possible to create meaningless terms containing loose bound vars
   or type mismatches.  But such terms are not allowed in rules. *)
 
 datatype term =
     Const of string * typ
   | Free  of string * typ
   | Var   of indexname * typ
   | Bound of int
   | Abs   of string*typ*term
   | op $  of term*term;
 
 (*Errors involving type mismatches*)
 exception TYPE of string * typ list * term list;
 
 (*Errors errors involving terms*)
 exception TERM of string * term list;
 
 (*Note variable naming conventions!
     a,b,c: string
     f,g,h: functions (including terms of function type)
     i,j,m,n: int
     t,u: term
     v,w: indexnames
     x,y: any
     A,B,C: term (denoting formulae)
     T,U: typ
 *)
 
 
 (** Types **)
 
 (*dummies for type-inference etc.*)
 val dummyS = [""];
 val dummyT = Type ("dummy", []);
 
 fun no_dummyT typ =
   let
     fun check (T as Type ("dummy", _)) =
           raise TYPE ("Illegal occurrence of '_' dummy type", [T], [])
       | check (Type (_, Ts)) = List.app check Ts
       | check _ = ();
   in check typ; typ end;
 
 fun S --> T = Type("fun",[S,T]);
 
 (*handy for multiple args: [T1,...,Tn]--->T  gives  T1-->(T2--> ... -->T)*)
 val op ---> = Library.foldr (op -->);
 
 
 (** Discriminators **)
 
 fun is_Type (Type _) = true
   | is_Type _ = false;
 
 fun is_TFree (TFree _) = true
   | is_TFree _ = false;
 
 fun is_TVar (TVar _) = true
   | is_TVar _ = false;
 
 
 (** Destructors **)
 
 fun dest_Type (Type x) = x
   | dest_Type T = raise TYPE ("dest_Type", [T], []);
 
 fun dest_TFree (TFree x) = x
   | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
 
 fun dest_TVar (TVar x) = x
   | dest_TVar T = raise TYPE ("dest_TVar", [T], []);
 
 
 (** Discriminators **)
 
 fun is_Bound (Bound _) = true
   | is_Bound _         = false;
 
 fun is_Const (Const _) = true
   | is_Const _ = false;
 
 fun is_Free (Free _) = true
   | is_Free _ = false;
 
 fun is_Var (Var _) = true
   | is_Var _ = false;
 
 
 (** Destructors **)
 
 fun dest_Const (Const x) =  x
   | dest_Const t = raise TERM("dest_Const", [t]);
 
 fun dest_Free (Free x) =  x
   | dest_Free t = raise TERM("dest_Free", [t]);
 
 fun dest_Var (Var x) =  x
   | dest_Var t = raise TERM("dest_Var", [t]);
 
 fun dest_comb (t1 $ t2) = (t1, t2)
   | dest_comb t = raise TERM("dest_comb", [t]);
 
 
 fun domain_type (Type ("fun", [T, _])) = T;
 
 fun range_type (Type ("fun", [_, U])) = U;
 
 fun dest_funT (Type ("fun", [T, U])) = (T, U)
   | dest_funT T = raise TYPE ("dest_funT", [T], []);
 
 
 (*maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
   | binder_types _ = [];
 
 (*maps  [T1,...,Tn]--->T  to T*)
 fun body_type (Type ("fun", [_, U])) = body_type U
   | body_type T = T;
 
 (*maps  [T1,...,Tn]--->T  to   ([T1,T2,...,Tn], T)*)
 fun strip_type T = (binder_types T, body_type T);
 
 
 (*Compute the type of the term, checking that combinations are well-typed
   Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)
 fun type_of1 (Ts, Const (_,T)) = T
   | type_of1 (Ts, Free  (_,T)) = T
   | type_of1 (Ts, Bound i) = (nth Ts i
         handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
   | type_of1 (Ts, Var (_,T)) = T
   | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
   | type_of1 (Ts, f$u) =
       let val U = type_of1(Ts,u)
           and T = type_of1(Ts,f)
       in case T of
             Type("fun",[T1,T2]) =>
               if T1=U then T2  else raise TYPE
                     ("type_of: type mismatch in application", [T1,U], [f$u])
           | _ => raise TYPE
                     ("type_of: function type is expected in application",
                      [T,U], [f$u])
       end;
 
 fun type_of t : typ = type_of1 ([],t);
 
 (*Determine the type of a term, with minimal checking*)
 local
 
 fun fastype_of_term Ts (Abs (_, T, t)) = T --> fastype_of_term (T :: Ts) t
   | fastype_of_term Ts (t $ _) = range_type_of Ts t
   | fastype_of_term Ts a = fastype_of_atom Ts a
 and fastype_of_atom _ (Const (_, T)) = T
   | fastype_of_atom _ (Free (_, T)) = T
   | fastype_of_atom _ (Var (_, T)) = T
   | fastype_of_atom Ts (Bound i) = fastype_of_bound Ts i
 and fastype_of_bound (T :: Ts) i = if i = 0 then T else fastype_of_bound Ts (i - 1)
   | fastype_of_bound [] i = raise TERM ("fastype_of: Bound", [Bound i])
 and range_type_of Ts (Abs (_, T, u)) = fastype_of_term (T :: Ts) u
   | range_type_of Ts (t $ u) = range_type_ofT (t $ u) (range_type_of Ts t)
   | range_type_of Ts a = range_type_ofT a (fastype_of_atom Ts a)
 and range_type_ofT _ (Type ("fun", [_, T])) = T
   | range_type_ofT t _ = raise TERM ("fastype_of: expected function type", [t]);
 
 in
 
 val fastype_of1 = uncurry fastype_of_term;
 val fastype_of = fastype_of_term [];
 
 end;
 
 (*Determine the argument type of a function*)
 fun argument_type_of tm k =
   let
     fun argT i (Type ("fun", [T, U])) = if i = 0 then T else argT (i - 1) U
       | argT _ T = raise TYPE ("argument_type_of", [T], []);
 
     fun arg 0 _ (Abs (_, T, _)) = T
       | arg i Ts (Abs (_, T, t)) = arg (i - 1) (T :: Ts) t
       | arg i Ts (t $ _) = arg (i + 1) Ts t
       | arg i Ts a = argT i (fastype_of1 (Ts, a));
   in arg k [] tm end;
 
 
 fun abs (x, T) t = Abs (x, T, t);
 
 fun strip_abs (Abs (a, T, t)) =
       let val (a', t') = strip_abs t
       in ((a, T) :: a', t') end
   | strip_abs t = ([], t);
 
 (*maps  (x1,...,xn)t   to   t*)
 fun strip_abs_body (Abs(_,_,t))  =  strip_abs_body t
   | strip_abs_body u  =  u;
 
 (*maps  (x1,...,xn)t   to   [x1, ..., xn]*)
 fun strip_abs_vars (Abs(a,T,t))  =  (a,T) :: strip_abs_vars t
   | strip_abs_vars u  =  [] : (string*typ) list;
 
 
 fun strip_qnt_body qnt =
 let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm
       | strip t = t
 in strip end;
 
 fun strip_qnt_vars qnt =
 let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []
       | strip t  =  [] : (string*typ) list
 in strip end;
 
 
 (*maps   (f, [t1,...,tn])  to  f(t1,...,tn)*)
 val list_comb : term * term list -> term = Library.foldl (op $);
 
 
 (*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*)
 fun strip_comb u : term * term list =
     let fun stripc (f$t, ts) = stripc (f, t::ts)
         |   stripc  x =  x
     in  stripc(u,[])  end;
 
 
 (*maps   f(t1,...,tn)  to  f , which is never a combination*)
 fun head_of (f$t) = head_of f
   | head_of u = u;
 
 (*number of atoms and abstractions in a term*)
 fun size_of_term tm =
   let
     fun add_size (t $ u) n = add_size t (add_size u n)
       | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
       | add_size _ n = n + 1;
   in add_size tm 0 end;
 
 (*number of atoms and constructors in a type*)
 fun size_of_typ ty =
   let
     fun add_size (Type (_, tys)) n = fold add_size tys (n + 1)
       | add_size _ n = n + 1;
   in add_size ty 0 end;
 
 fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts)
   | map_atyps f T = f T;
 
 fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u
   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   | map_aterms f t = f t;
 
 fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
 fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
 
 fun map_types f =
   let
     fun map_aux (Const (a, T)) = Const (a, f T)
       | map_aux (Free (a, T)) = Free (a, f T)
       | map_aux (Var (v, T)) = Var (v, f T)
       | map_aux (Bound i) = Bound i
       | map_aux (Abs (a, T, t)) = Abs (a, f T, map_aux t)
       | map_aux (t $ u) = map_aux t $ map_aux u;
   in map_aux end;
 
 
 (* fold types and terms *)
 
 fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
   | fold_atyps f T = f T;
 
 fun fold_atyps_sorts f =
   fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
 
 fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
   | fold_aterms f (Abs (_, _, t)) = fold_aterms f t
   | fold_aterms f a = f a;
 
 fun fold_term_types f (t as Const (_, T)) = f t T
   | fold_term_types f (t as Free (_, T)) = f t T
   | fold_term_types f (t as Var (_, T)) = f t T
   | fold_term_types f (Bound _) = I
   | fold_term_types f (t as Abs (_, T, b)) = f t T #> fold_term_types f b
   | fold_term_types f (t $ u) = fold_term_types f t #> fold_term_types f u;
 
 fun fold_types f = fold_term_types (K f);
 
 fun replace_types (Const (c, _)) (T :: Ts) = (Const (c, T), Ts)
   | replace_types (Free (x, _)) (T :: Ts) = (Free (x, T), Ts)
   | replace_types (Var (xi, _)) (T :: Ts) = (Var (xi, T), Ts)
   | replace_types (Bound i) Ts = (Bound i, Ts)
   | replace_types (Abs (x, _, b)) (T :: Ts) =
       let val (b', Ts') = replace_types b Ts
       in (Abs (x, T, b'), Ts') end
   | replace_types (t $ u) Ts =
       let
         val (t', Ts') = replace_types t Ts;
         val (u', Ts'') = replace_types u Ts';
       in (t' $ u', Ts'') end;
 
 fun burrow_types f ts =
   let
     val Ts = rev ((fold o fold_types) cons ts []);
     val Ts' = f Ts;
     val (ts', []) = fold_map replace_types ts Ts';
   in ts' end;
 
 (*collect variables*)
 val add_tvar_namesT = fold_atyps (fn TVar (xi, _) => insert (op =) xi | _ => I);
 val add_tvar_names = fold_types add_tvar_namesT;
 val add_tvarsT = fold_atyps (fn TVar v => insert (op =) v | _ => I);
 val add_tvars = fold_types add_tvarsT;
 val add_var_names = fold_aterms (fn Var (xi, _) => insert (op =) xi | _ => I);
 val add_vars = fold_aterms (fn Var v => insert (op =) v | _ => I);
 val add_tfree_namesT = fold_atyps (fn TFree (a, _) => insert (op =) a | _ => I);
 val add_tfree_names = fold_types add_tfree_namesT;
 val add_tfreesT = fold_atyps (fn TFree v => insert (op =) v | _ => I);
 val add_tfrees = fold_types add_tfreesT;
 val add_free_names = fold_aterms (fn Free (x, _) => insert (op =) x | _ => I);
 val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
 val add_const_names = fold_aterms (fn Const (c, _) => insert (op =) c | _ => I);
 val add_consts = fold_aterms (fn Const c => insert (op =) c | _ => I);
 
 (*extra type variables in a term, not covered by its type*)
 fun hidden_polymorphism t =
   let
     val T = fastype_of t;
     val tvarsT = add_tvarsT T [];
     val extra_tvars = fold_types (fold_atyps
       (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
   in extra_tvars end;
 
 
 (* renaming variables *)
 
 val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
 
 fun declare_term_names tm =
   fold_aterms
     (fn Const (a, _) => Name.declare (Long_Name.base_name a)
       | Free (a, _) => Name.declare a
       | _ => I) tm #>
   fold_types declare_typ_names tm;
 
 val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
 
 fun variant_frees t frees =
   fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
     map snd frees;
 
 fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
 
 
 
 (** Comparing terms **)
 
 (* variables *)
 
 fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
 
 fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
 fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
 
 
 (* alpha equivalence *)
 
 fun tm1 aconv tm2 =
   pointer_eq (tm1, tm2) orelse
     (case (tm1, tm2) of
       (t1 $ u1, t2 $ u2) => t1 aconv t2 andalso u1 aconv u2
     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
     | (a1, a2) => a1 = a2);
 
 fun aconv_untyped (tm1, tm2) =
   pointer_eq (tm1, tm2) orelse
     (case (tm1, tm2) of
       (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
     | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
     | (Const (a, _), Const (b, _)) => a = b
     | (Free (x, _), Free (y, _)) => x = y
     | (Var (xi, _), Var (yj, _)) => xi = yj
     | (Bound i, Bound j) => i = j
     | _ => false);
 
 
 (*A fast unification filter: true unless the two terms cannot be unified.
   Terms must be NORMAL.  Treats all Vars as distinct. *)
 fun could_unify (t, u) =
   let
     fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
       | matchrands _ _ = true;
   in
     case (head_of t, head_of u) of
       (_, Var _) => true
     | (Var _, _) => true
     | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
     | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
     | (Bound i, Bound j) => i = j andalso matchrands t u
     | (Abs _, _) => true   (*because of possible eta equality*)
     | (_, Abs _) => true
     | _ => false
   end;
 
 
 
 (** Connectives of higher order logic **)
 
 fun aT S = TFree (Name.aT, S);
 
 fun itselfT ty = Type ("itself", [ty]);
 val a_itselfT = itselfT (TFree (Name.aT, []));
 
 val propT : typ = Type ("prop",[]);
 
 (*maps  \<And>x1...xn. t   to   t*)
 fun strip_all_body (Const ("Pure.all", _) $ Abs (_, _, t)) = strip_all_body t
   | strip_all_body t = t;
 
 (*maps  \<And>x1...xn. t   to   [x1, ..., xn]*)
 fun strip_all_vars (Const ("Pure.all", _) $ Abs (a, T, t)) = (a, T) :: strip_all_vars t
   | strip_all_vars t = [];
 
 (*increments a term's non-local bound variables
   required when moving a term within abstractions
      inc is  increment for bound variables
      lev is  level at which a bound variable is considered 'loose'*)
 fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u
   | incr_bv (inc, lev, Abs(a,T,body)) =
         Abs(a, T, incr_bv(inc,lev+1,body))
   | incr_bv (inc, lev, f$t) =
       incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)
   | incr_bv (inc, lev, u) = u;
 
 fun incr_boundvars  0  t = t
   | incr_boundvars inc t = incr_bv(inc,0,t);
 
 (*Scan a pair of terms; while they are similar,
   accumulate corresponding bound vars in "al"*)
 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) =
       match_bvs(s, t, if x="" orelse y="" then al
                                           else (x,y)::al)
   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   | match_bvs(_,_,al) = al;
 
 (* strip abstractions created by parameters *)
 fun match_bvars (s,t) al = match_bvs(strip_abs_body s, strip_abs_body t, al);
 
 fun map_abs_vars f (t $ u) = map_abs_vars f t $ map_abs_vars f u
   | map_abs_vars f (Abs (a, T, t)) = Abs (f a, T, map_abs_vars f t)
   | map_abs_vars f t = t;
 
 fun rename_abs pat obj t =
   let
     val ren = match_bvs (pat, obj, []);
     fun ren_abs (Abs (x, T, b)) =
           Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
       | ren_abs (f $ t) = ren_abs f $ ren_abs t
       | ren_abs t = t
   in if null ren then NONE else SOME (ren_abs t) end;
 
 (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    (Bound 0) is loose at level 0 *)
 fun add_loose_bnos (Bound i, lev, js) =
         if i<lev then js else insert (op =) (i - lev) js
   | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   | add_loose_bnos (f$t, lev, js) =
         add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   | add_loose_bnos (_, _, js) = js;
 
 fun loose_bnos t = add_loose_bnos (t, 0, []);
 
 (* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to
    level k or beyond. *)
 fun loose_bvar(Bound i,k) = i >= k
   | loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)
   | loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)
   | loose_bvar _ = false;
 
 fun loose_bvar1(Bound i,k) = i = k
   | loose_bvar1(f$t, k) = loose_bvar1(f,k) orelse loose_bvar1(t,k)
   | loose_bvar1(Abs(_,_,t),k) = loose_bvar1(t,k+1)
   | loose_bvar1 _ = false;
 
 fun is_open t = loose_bvar (t, 0);
 fun is_dependent t = loose_bvar1 (t, 0);
 
 (*Substitute arguments for loose bound variables.
   Beta-reduction of arg(n-1)...arg0 into t replacing (Bound i) with (argi).
   Note that for ((\<lambda>x y. c) a b), the bound vars in c are x=1 and y=0
         and the appropriate call is  subst_bounds([b,a], c) .
   Loose bound variables >=n are reduced by "n" to
      compensate for the disappearance of lambdas.
 *)
 fun subst_bounds (args: term list, t) : term =
   let
     val n = length args;
     fun subst (t as Bound i, lev) =
          (if i < lev then raise Same.SAME   (*var is locally bound*)
           else incr_boundvars lev (nth args (i - lev))
             handle General.Subscript => Bound (i - n))  (*loose: change it*)
       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
       | subst (f $ t, lev) =
           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
             handle Same.SAME => f $ subst (t, lev))
       | subst _ = raise Same.SAME;
   in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
 
 (*Special case: one argument*)
 fun subst_bound (arg, t) : term =
   let
     fun subst (Bound i, lev) =
           if i < lev then raise Same.SAME   (*var is locally bound*)
           else if i = lev then incr_boundvars lev arg
           else Bound (i - 1)   (*loose: change it*)
       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
       | subst (f $ t, lev) =
           (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
             handle Same.SAME => f $ subst (t, lev))
       | subst _ = raise Same.SAME;
   in subst (t, 0) handle Same.SAME => t end;
 
 (*beta-reduce if possible, else form application*)
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
   | betapply (f,u) = f$u;
 
 val betapplys = Library.foldl betapply;
 
 
 (*unfolding abstractions with substitution
   of bound variables and implicit eta-expansion*)
 fun strip_abs_eta k t =
   let
     val used = fold_aterms declare_term_frees t Name.context;
     fun strip_abs t (0, used) = (([], t), (0, used))
       | strip_abs (Abs (v, T, t)) (k, used) =
           let
             val (v', used') = Name.variant v used;
             val t' = subst_bound (Free (v', T), t);
             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
           in (((v', T) :: vs, t''), (k', used'')) end
       | strip_abs t (k, used) = (([], t), (k, used));
     fun expand_eta [] t _ = ([], t)
       | expand_eta (T::Ts) t used =
           let
             val (v, used') = Name.variant "" used;
             val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
           in ((v, T) :: vs, t') end;
     val ((vs1, t'), (k', used')) = strip_abs t (k, used);
     val Ts = fst (chop k' (binder_types (fastype_of t')));
     val (vs2, t'') = expand_eta Ts t' used';
   in (vs1 @ vs2, t'') end;
 
 
 (*Substitute new for free occurrences of old in a term*)
 fun subst_free [] = I
   | subst_free pairs =
       let fun substf u =
             case AList.lookup (op aconv) pairs u of
                 SOME u' => u'
               | NONE => (case u of Abs(a,T,t) => Abs(a, T, substf t)
                                  | t$u' => substf t $ substf u'
                                  | _ => u)
       in  substf  end;
 
 (*Abstraction of the term "body" over its occurrences of v,
     which must contain no loose bound variables.
   The resulting term is ready to become the body of an Abs.*)
 fun abstract_over (v, body) =
   let
     fun abs lev tm =
       if v aconv tm then Bound lev
       else
         (case tm of
           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
         | t $ u =>
             (abs lev t $ (abs lev u handle Same.SAME => u)
               handle Same.SAME => t $ abs lev u)
         | _ => raise Same.SAME);
   in abs 0 body handle Same.SAME => body end;
 
 fun term_name (Const (x, _)) = Long_Name.base_name x
   | term_name (Free (x, _)) = x
   | term_name (Var ((x, _), _)) = x
   | term_name _ = Name.uu;
 
 fun dependent_lambda_name (x, v) t =
   let val t' = abstract_over (v, t)
   in if is_dependent t' then Abs (if x = "" then term_name v else x, fastype_of v, t') else t end;
 
 fun lambda_name (x, v) t =
   Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
 
 fun lambda v t = lambda_name ("", v) t;
 
 fun absfree (a, T) body = Abs (a, T, abstract_over (Free (a, T), body));
 fun absdummy T body = Abs (Name.uu_, T, body);
 
 (*Replace the ATOMIC term ti by ui;    inst = [(t1,u1), ..., (tn,un)].
   A simultaneous substitution:  [ (a,b), (b,a) ] swaps a and b.  *)
 fun subst_atomic [] tm = tm
   | subst_atomic inst tm =
       let
         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
           | subst (t $ u) = subst t $ subst u
           | subst t = the_default t (AList.lookup (op aconv) inst t);
       in subst tm end;
 
 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
 fun typ_subst_atomic [] ty = ty
   | typ_subst_atomic inst ty =
       let
         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
           | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
       in subst ty end;
 
 fun subst_atomic_types [] tm = tm
   | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
 
 fun typ_subst_TVars [] ty = ty
   | typ_subst_TVars inst ty =
       let
         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
           | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
           | subst T = T;
       in subst ty end;
 
 fun subst_TVars [] tm = tm
   | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
 
 fun subst_Vars [] tm = tm
   | subst_Vars inst tm =
       let
         fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
           | subst (t $ u) = subst t $ subst u
           | subst t = t;
       in subst tm end;
 
 fun subst_vars ([], []) tm = tm
   | subst_vars ([], inst) tm = subst_Vars inst tm
   | subst_vars (instT, inst) tm =
       let
         fun subst (Const (a, T)) = Const (a, typ_subst_TVars instT T)
           | subst (Free (a, T)) = Free (a, typ_subst_TVars instT T)
           | subst (Var (xi, T)) =
               (case AList.lookup (op =) inst xi of
                 NONE => Var (xi, typ_subst_TVars instT T)
               | SOME t => t)
           | subst (t as Bound _) = t
           | subst (Abs (a, T, t)) = Abs (a, typ_subst_TVars instT T, subst t)
           | subst (t $ u) = subst t $ subst u;
       in subst tm end;
 
 fun close_schematic_term t =
   let
     val extra_types = map (fn v => Const ("Pure.type", itselfT (TVar v))) (hidden_polymorphism t);
     val extra_terms = map Var (add_vars t []);
   in fold lambda (extra_terms @ extra_types) t end;
 
 
 
 (** Identifying first-order terms **)
 
 (*Differs from proofterm/is_fun in its treatment of TVar*)
 fun is_funtype (Type ("fun", [_, _])) = true
   | is_funtype _ = false;
 
 (*Argument Ts is a reverse list of binder types, needed if term t contains Bound vars*)
 fun has_not_funtype Ts t = not (is_funtype (fastype_of1 (Ts, t)));
 
 (*First order means in all terms of the form f(t1,...,tn) no argument has a
   function type. The supplied quantifiers are excluded: their argument always
   has a function type through a recursive call into its body.*)
 fun is_first_order quants =
   let fun first_order1 Ts (Abs (_,T,body)) = first_order1 (T::Ts) body
         | first_order1 Ts (Const(q,_) $ Abs(a,T,body)) =
             member (op =) quants q  andalso   (*it is a known quantifier*)
             not (is_funtype T)   andalso first_order1 (T::Ts) body
         | first_order1 Ts t =
             case strip_comb t of
                  (Var _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
                | (Free _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
                | (Const _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
                | (Bound _, ts) => forall (first_order1 Ts andf has_not_funtype Ts) ts
                | (Abs _, ts) => false (*not in beta-normal form*)
                | _ => error "first_order: unexpected case"
     in  first_order1 []  end;
 
 
 (* maximum index of typs and terms *)
 
 fun maxidx_typ (TVar ((_, j), _)) i = Int.max (i, j)
   | maxidx_typ (Type (_, Ts)) i = maxidx_typs Ts i
   | maxidx_typ (TFree _) i = i
 and maxidx_typs [] i = i
   | maxidx_typs (T :: Ts) i = maxidx_typs Ts (maxidx_typ T i);
 
 fun maxidx_term (Var ((_, j), T)) i = maxidx_typ T (Int.max (i, j))
   | maxidx_term (Const (_, T)) i = maxidx_typ T i
   | maxidx_term (Free (_, T)) i = maxidx_typ T i
   | maxidx_term (Bound _) i = i
   | maxidx_term (Abs (_, T, t)) i = maxidx_term t (maxidx_typ T i)
   | maxidx_term (t $ u) i = maxidx_term u (maxidx_term t i);
 
 fun maxidx_of_typ T = maxidx_typ T ~1;
 fun maxidx_of_typs Ts = maxidx_typs Ts ~1;
 fun maxidx_of_term t = maxidx_term t ~1;
 
 
 
 (** misc syntax operations **)
 
 (* substructure *)
 
 fun fold_subtypes f =
   let
     fun iter ty =
       (case ty of Type (_, Ts) => f ty #> fold iter Ts | _ => f ty);
   in iter end;
 
 fun exists_subtype P =
   let
     fun ex ty = P ty orelse
       (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   in ex end;
 
 fun exists_type P =
   let
     fun ex (Const (_, T)) = P T
       | ex (Free (_, T)) = P T
       | ex (Var (_, T)) = P T
       | ex (Bound _) = false
       | ex (Abs (_, T, t)) = P T orelse ex t
       | ex (t $ u) = ex t orelse ex u;
   in ex end;
 
 fun exists_subterm P =
   let
     fun ex tm = P tm orelse
       (case tm of
         t $ u => ex t orelse ex u
       | Abs (_, _, t) => ex t
       | _ => false);
   in ex end;
 
 fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
 
 
 (* contraction *)
 
 fun could_beta_contract (Abs _ $ _) = true
   | could_beta_contract (t $ u) = could_beta_contract t orelse could_beta_contract u
   | could_beta_contract (Abs (_, _, b)) = could_beta_contract b
   | could_beta_contract _ = false;
 
 fun could_eta_contract (Abs (_, _, _ $ Bound 0)) = true
   | could_eta_contract (Abs (_, _, b)) = could_eta_contract b
   | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u
   | could_eta_contract _ = false;
 
 fun could_beta_eta_contract (Abs _ $ _) = true
   | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true
   | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b
   | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u
   | could_beta_eta_contract _ = false;
 
 
 (* dest abstraction *)
 
 fun used_free x =
   let
     fun used (Free (y, _)) = (x = y)
       | used (t $ u) = used t orelse used u
       | used (Abs (_, _, t)) = used t
       | used _ = false;
   in used end;
 
 fun dest_abs (x, T, b) =
   if used_free x b then
     let val (x', _) = Name.variant x (declare_term_frees b Name.context);
     in (x', subst_bound (Free (x', T), b)) end
   else (x, subst_bound (Free (x, T), b));
 
 
 (* dummy patterns *)
 
 fun dummy_pattern T = Const ("Pure.dummy_pattern", T);
 val dummy = dummy_pattern dummyT;
 val dummy_prop = dummy_pattern propT;
 
 fun is_dummy_pattern (Const ("Pure.dummy_pattern", _)) = true
   | is_dummy_pattern _ = false;
 
 fun no_dummy_patterns tm =
   if not (fold_aterms (fn t => fn b => b orelse is_dummy_pattern t) tm false) then tm
   else raise TERM ("Illegal occurrence of '_' dummy pattern", [tm]);
 
 fun free_dummy_patterns (Const ("Pure.dummy_pattern", T)) used =
       let val [x] = Name.invent used Name.uu 1
       in (Free (Name.internal x, T), Name.declare x used) end
   | free_dummy_patterns (Abs (x, T, b)) used =
       let val (b', used') = free_dummy_patterns b used
       in (Abs (x, T, b'), used') end
   | free_dummy_patterns (t $ u) used =
       let
         val (t', used') = free_dummy_patterns t used;
         val (u', used'') = free_dummy_patterns u used';
       in (t' $ u', used'') end
   | free_dummy_patterns a used = (a, used);
 
 fun replace_dummy Ts (Const ("Pure.dummy_pattern", T)) i =
       (list_comb (Var (("_dummy_", i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   | replace_dummy Ts (Abs (x, T, t)) i =
       let val (t', i') = replace_dummy (T :: Ts) t i
       in (Abs (x, T, t'), i') end
   | replace_dummy Ts (t $ u) i =
       let
         val (t', i') = replace_dummy Ts t i;
         val (u', i'') = replace_dummy Ts u i';
       in (t' $ u', i'') end
   | replace_dummy _ a i = (a, i);
 
 val replace_dummy_patterns = replace_dummy [];
 
 fun show_dummy_patterns (Var (("_dummy_", _), T)) = dummy_pattern T
   | show_dummy_patterns (t $ u) = show_dummy_patterns t $ show_dummy_patterns u
   | show_dummy_patterns (Abs (x, T, t)) = Abs (x, T, show_dummy_patterns t)
   | show_dummy_patterns a = a;
 
 
 (* display variables *)
 
 fun string_of_vname (x, i) =
   let
     val idx = string_of_int i;
     val dot =
       (case rev (Symbol.explode x) of
         _ :: "\<^sub>" :: _ => false
       | c :: _ => Symbol.is_digit c
       | _ => true);
   in
     if dot then "?" ^ x ^ "." ^ idx
     else if i <> 0 then "?" ^ x ^ idx
     else "?" ^ x
   end;
 
 fun string_of_vname' (x, ~1) = x
   | string_of_vname' xi = string_of_vname xi;
 
 end;
 
 structure Basic_Term: BASIC_TERM = Term;
 open Basic_Term;
diff --git a/src/Tools/Code/code_thingol.ML b/src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML
+++ b/src/Tools/Code/code_thingol.ML
@@ -1,1043 +1,1042 @@
 (*  Title:      Tools/Code/code_thingol.ML
     Author:     Florian Haftmann, TU Muenchen
 
 Intermediate language ("Thin-gol") representing executable code.
 Representation and translation.
 *)
 
 infix 8 `%%;
 infix 4 `$;
 infix 4 `$$;
 infixr 3 `->;
 infixr 3 `|=>;
 infixr 3 `|==>;
 
 signature BASIC_CODE_THINGOL =
 sig
   type vname = string;
   datatype dict =
       Dict of (class * class) list * plain_dict
   and plain_dict = 
       Dict_Const of (string * class) * dict list list
     | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
   datatype itype =
       `%% of string * itype list
     | ITyVar of vname;
   type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
     dom: itype list, annotation: itype option };
   datatype iterm =
       IConst of const
     | IVar of vname option
     | `$ of iterm * iterm
     | `|=> of (vname option * itype) * iterm
     | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
   val `-> : itype * itype -> itype;
   val `$$ : iterm * iterm list -> iterm;
   val `|==> : (vname option * itype) list * iterm -> iterm;
   type typscheme = (vname * sort) list * itype;
 end;
 
 signature CODE_THINGOL =
 sig
   include BASIC_CODE_THINGOL
   val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list
   val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a
   val unfold_fun: itype -> itype list * itype
   val unfold_fun_n: int -> itype -> itype list * itype
   val unfold_app: iterm -> iterm * iterm list
   val unfold_abs: iterm -> (vname option * itype) list * iterm
   val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
   val split_let_no_pat: iterm -> (((string option * itype) * iterm) * iterm) option
   val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
   val unfold_let_no_pat: iterm -> ((string option * itype) * iterm) list * iterm
   val split_pat_abs: iterm -> ((iterm * itype) * iterm) option
   val unfold_pat_abs: iterm -> (iterm * itype) list * iterm
   val unfold_const_app: iterm -> (const * iterm list) option
   val is_IVar: iterm -> bool
   val is_IAbs: iterm -> bool
   val eta_expand: int -> const * iterm list -> iterm
   val contains_dict_var: iterm -> bool
   val unambiguous_dictss: dict list list -> bool
   val add_constsyms: iterm -> Code_Symbol.T list -> Code_Symbol.T list
   val add_tyconames: iterm -> string list -> string list
   val fold_varnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
 
   datatype stmt =
       NoStmt
     | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
     | Datatype of vname list *
         ((string * vname list (*type argument wrt. canonical order*)) * itype list) list
     | Datatypecons of string
     | Class of vname * ((class * class) list * (string * itype) list)
     | Classrel of class * class
     | Classparam of class
     | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
         superinsts: (class * dict list list) list,
         inst_params: ((string * (const * int)) * (thm * bool)) list,
         superinst_params: ((string * (const * int)) * (thm * bool)) list };
   type program = stmt Code_Symbol.Graph.T
   val unimplemented: program -> string list
   val implemented_deps: program -> string list
   val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
   val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
   val is_constr: program -> Code_Symbol.T -> bool
   val is_case: stmt -> bool
   val group_stmts: Proof.context -> program
     -> ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list
       * ((Code_Symbol.T * stmt) list * (Code_Symbol.T * stmt) list)) list
 
   val read_const_exprs: Proof.context -> string list -> string list
   val consts_program: Proof.context -> string list -> program
   val dynamic_conv: Proof.context -> (program
     -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> conv
   val dynamic_value: Proof.context -> ((term -> term) -> 'a -> 'a) -> (program
     -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> term -> 'a
   val static_conv_thingol: { ctxt: Proof.context, consts: string list }
     -> ({ program: program, deps: string list }
       -> Proof.context -> typscheme * iterm -> Code_Symbol.T list -> conv)
     -> Proof.context -> conv
   val static_conv_isa: { ctxt: Proof.context, consts: string list }
     -> (program -> Proof.context -> term -> conv)
     -> Proof.context -> conv
   val static_value: { ctxt: Proof.context, lift_postproc: ((term -> term) -> 'a -> 'a), consts: string list }
     -> ({ program: program, deps: string list }
       -> Proof.context -> term -> typscheme * iterm -> Code_Symbol.T list -> 'a)
     -> Proof.context -> term -> 'a
 end;
 
 structure Code_Thingol : CODE_THINGOL =
 struct
 
 open Basic_Code_Symbol;
 
 (** auxiliary **)
 
 fun unfoldl dest x =
   case dest x
    of NONE => (x, [])
     | SOME (x1, x2) =>
         let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
 
 fun unfoldr dest x =
   case dest x
    of NONE => ([], x)
     | SOME (x1, x2) =>
         let val (xs', x') = unfoldr dest x2 in (x1 :: xs', x') end;
 
 
 (** language core - types, terms **)
 
 type vname = string;
 
 datatype dict =
     Dict of (class * class) list * plain_dict
 and plain_dict = 
     Dict_Const of (string * class) * dict list list
   | Dict_Var of { var: vname, index: int, length: int, class: class, unique: bool };
 
 datatype itype =
     `%% of string * itype list
   | ITyVar of vname;
 
 fun ty1 `-> ty2 = "fun" `%% [ty1, ty2];
 
 val unfold_fun = unfoldr
   (fn "fun" `%% [ty1, ty2] => SOME (ty1, ty2)
     | _ => NONE);
 
 fun unfold_fun_n n ty =
   let
     val (tys1, ty1) = unfold_fun ty;
     val (tys3, tys2) = chop n tys1;
     val ty3 = Library.foldr (op `->) (tys2, ty1);
   in (tys3, ty3) end;
 
 type const = { sym: Code_Symbol.T, typargs: itype list, dicts: dict list list,
   dom: itype list, annotation: itype option };
 
 datatype iterm =
     IConst of const
   | IVar of vname option
   | `$ of iterm * iterm
   | `|=> of (vname option * itype) * iterm
   | ICase of { term: iterm, typ: itype, clauses: (iterm * iterm) list, primitive: iterm };
     (*see also signature*)
 
 fun is_IVar (IVar _) = true
   | is_IVar _ = false;
 
 fun is_IAbs (_ `|=> _) = true
   | is_IAbs _ = false;
 
 val op `$$ = Library.foldl (op `$);
 val op `|==> = Library.foldr (op `|=>);
 
 val unfold_app = unfoldl
   (fn op `$ t => SOME t
     | _ => NONE);
 
 val unfold_abs = unfoldr
   (fn op `|=> t => SOME t
     | _ => NONE);
 
 val split_let = 
   (fn ICase { term = t, typ = ty, clauses = [(p, body)], ... } => SOME (((p, ty), t), body)
     | _ => NONE);
 
 val split_let_no_pat = 
   (fn ICase { term = t, typ = ty, clauses = [(IVar v, body)], ... } => SOME (((v, ty), t), body)
     | _ => NONE);
 
 val unfold_let = unfoldr split_let;
 
 val unfold_let_no_pat = unfoldr split_let_no_pat;
 
 fun unfold_const_app t =
  case unfold_app t
   of (IConst c, ts) => SOME (c, ts)
    | _ => NONE;
 
 fun fold_constexprs f =
   let
     fun fold' (IConst c) = f c
       | fold' (IVar _) = I
       | fold' (t1 `$ t2) = fold' t1 #> fold' t2
       | fold' (_ `|=> t) = fold' t
       | fold' (ICase { term = t, clauses = clauses, ... }) = fold' t
           #> fold (fn (p, body) => fold' p #> fold' body) clauses
   in fold' end;
 
 val add_constsyms = fold_constexprs (fn { sym, ... } => insert (op =) sym);
 
 fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
   | add_tycos (ITyVar _) = I;
 
 val add_tyconames = fold_constexprs (fn { typargs = tys, ... } => fold add_tycos tys);
 
 fun fold_varnames f =
   let
     fun fold_aux add_vars f =
       let
         fun fold_term _ (IConst _) = I
           | fold_term vs (IVar (SOME v)) = if member (op =) vs v then I else f v
           | fold_term _ (IVar NONE) = I
           | fold_term vs (t1 `$ t2) = fold_term vs t1 #> fold_term vs t2
           | fold_term vs ((SOME v, _) `|=> t) = fold_term (insert (op =) v vs) t
           | fold_term vs ((NONE, _) `|=> t) = fold_term vs t
           | fold_term vs (ICase { term = t, clauses = clauses, ... }) =
               fold_term vs t #> fold (fold_clause vs) clauses
         and fold_clause vs (p, t) = fold_term (add_vars p vs) t;
       in fold_term [] end
     fun add_vars t = fold_aux add_vars (insert (op =)) t;
   in fold_aux add_vars f end;
 
 fun exists_var t v = fold_varnames (fn w => fn b => v = w orelse b) t false;
 
 fun split_pat_abs ((NONE, ty) `|=> t) = SOME ((IVar NONE, ty), t)
   | split_pat_abs ((SOME v, ty) `|=> t) = SOME (case t
      of ICase { term = IVar (SOME w), clauses = [(p, body)], ... } =>
           if v = w andalso (exists_var p v orelse not (exists_var body v))
           then ((p, ty), body)
           else ((IVar (SOME v), ty), t)
       | _ => ((IVar (SOME v), ty), t))
   | split_pat_abs _ = NONE;
 
 val unfold_pat_abs = unfoldr split_pat_abs;
 
 fun unfold_abs_eta [] t = ([], t)
   | unfold_abs_eta (_ :: tys) (v_ty `|=> t) =
       let
         val (vs_tys, t') = unfold_abs_eta tys t;
       in (v_ty :: vs_tys, t') end
   | unfold_abs_eta tys t =
       let
         val ctxt = fold_varnames Name.declare t Name.context;
         val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
       in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
 
 fun eta_expand k (const as { dom = tys, ... }, ts) =
   let
     val j = length ts;
     val l = k - j;
     val _ = if l > length tys
       then error "Impossible eta-expansion" else ();
     val vars = (fold o fold_varnames) Name.declare ts Name.context;
     val vs_tys = (map o apfst) SOME
       (Name.invent_names vars "a" ((take l o drop j) tys));
   in vs_tys `|==> IConst const `$$ ts @ map (IVar o fst) vs_tys end;
 
 fun exists_dict_var f (Dict (_, d)) = exists_plain_dict_var_pred f d
 and exists_plain_dict_var_pred f (Dict_Const (_, dss)) = exists_dictss_var f dss
   | exists_plain_dict_var_pred f (Dict_Var x) = f x
 and exists_dictss_var f dss = (exists o exists) (exists_dict_var f) dss;
 
 fun contains_dict_var (IConst { dicts = dss, ... }) = exists_dictss_var (K true) dss
   | contains_dict_var (IVar _) = false
   | contains_dict_var (t1 `$ t2) = contains_dict_var t1 orelse contains_dict_var t2
   | contains_dict_var (_ `|=> t) = contains_dict_var t
   | contains_dict_var (ICase { primitive = t, ... }) = contains_dict_var t;
 
 val unambiguous_dictss = not o exists_dictss_var (fn { unique, ... } => not unique);
 
 
 (** statements, abstract programs **)
 
 type typscheme = (vname * sort) list * itype;
 datatype stmt =
     NoStmt
   | Fun of (typscheme * ((iterm list * iterm) * (thm option * bool)) list) * thm option
   | Datatype of vname list * ((string * vname list) * itype list) list
   | Datatypecons of string
   | Class of vname * ((class * class) list * (string * itype) list)
   | Classrel of class * class
   | Classparam of class
   | Classinst of { class: string, tyco: string, vs: (vname * sort) list,
       superinsts: (class * dict list list) list,
       inst_params: ((string * (const * int)) * (thm * bool)) list,
       superinst_params: ((string * (const * int)) * (thm * bool)) list };
 
 type program = stmt Code_Symbol.Graph.T;
 
 fun unimplemented program =
   Code_Symbol.Graph.fold (fn (Constant c, (NoStmt, _)) => cons c | _ => I) program [];
 
 fun implemented_deps program =
   Code_Symbol.Graph.keys program
   |> subtract (op =) (Code_Symbol.Graph.all_preds program (map Constant (unimplemented program)))
   |> map_filter (fn Constant c => SOME c | _ => NONE);
 
 fun map_terms_bottom_up f (t as IConst _) = f t
   | map_terms_bottom_up f (t as IVar _) = f t
   | map_terms_bottom_up f (t1 `$ t2) = f
       (map_terms_bottom_up f t1 `$ map_terms_bottom_up f t2)
   | map_terms_bottom_up f ((v, ty) `|=> t) = f
       ((v, ty) `|=> map_terms_bottom_up f t)
   | map_terms_bottom_up f (ICase { term = t, typ = ty, clauses = clauses, primitive = t0 }) = f
       (ICase { term = map_terms_bottom_up f t, typ = ty,
         clauses = (map o apply2) (map_terms_bottom_up f) clauses,
         primitive = map_terms_bottom_up f t0 });
 
 fun map_classparam_instances_as_term f =
   (map o apfst o apsnd o apfst) (fn const => case f (IConst const) of IConst const' => const')
 
 fun map_terms_stmt f NoStmt = NoStmt
   | map_terms_stmt f (Fun ((tysm, eqs), case_cong)) = Fun ((tysm, (map o apfst)
       (fn (ts, t) => (map f ts, f t)) eqs), case_cong)
   | map_terms_stmt f (stmt as Datatype _) = stmt
   | map_terms_stmt f (stmt as Datatypecons _) = stmt
   | map_terms_stmt f (stmt as Class _) = stmt
   | map_terms_stmt f (stmt as Classrel _) = stmt
   | map_terms_stmt f (stmt as Classparam _) = stmt
   | map_terms_stmt f (Classinst { class, tyco, vs, superinsts,
       inst_params, superinst_params }) =
         Classinst { class = class, tyco = tyco, vs = vs, superinsts = superinsts,
           inst_params = map_classparam_instances_as_term f inst_params,
           superinst_params = map_classparam_instances_as_term f superinst_params };
 
 fun is_constr program sym = case Code_Symbol.Graph.get_node program sym
  of Datatypecons _ => true
   | _ => false;
 
 fun is_case (Fun (_, SOME _)) = true
   | is_case _ = false;
 
 fun linear_stmts program =
   rev (Code_Symbol.Graph.strong_conn program)
   |> map (AList.make (Code_Symbol.Graph.get_node program));
 
 fun group_stmts ctxt program =
   let
     fun is_fun (_, Fun _) = true | is_fun _ = false;
     fun is_datatypecons (_, Datatypecons _) = true | is_datatypecons _ = false;
     fun is_datatype (_, Datatype _) = true | is_datatype _ = false;
     fun is_class (_, Class _) = true | is_class _ = false;
     fun is_classrel (_, Classrel _) = true | is_classrel _ = false;
     fun is_classparam (_, Classparam _) = true | is_classparam _ = false;
     fun is_classinst (_, Classinst _) = true | is_classinst _ = false;
     fun group stmts =
       if forall (is_datatypecons orf is_datatype) stmts
       then (filter is_datatype stmts, [], ([], []))
       else if forall (is_class orf is_classrel orf is_classparam) stmts
       then ([], filter is_class stmts, ([], []))
       else if forall (is_fun orf is_classinst) stmts
       then ([], [], List.partition is_fun stmts)
       else error ("Illegal mutual dependencies: " ^ (commas
         o map (Code_Symbol.quote ctxt o fst)) stmts);
   in
     linear_stmts program
     |> map group
   end;
 
 
 (** translation kernel **)
 
 (* generic mechanisms *)
 
 fun ensure_stmt symbolize generate x (deps, program) =
   let
     val sym = symbolize x;
     val add_dep = case deps of [] => I
       | dep :: _ => Code_Symbol.Graph.add_edge (dep, sym);
   in
     if can (Code_Symbol.Graph.get_node program) sym
     then
       program
       |> add_dep
       |> pair deps
       |> pair x
     else
       program
       |> Code_Symbol.Graph.default_node (sym, NoStmt)
       |> add_dep
       |> curry generate (sym :: deps)
       ||> snd
       |-> (fn stmt => (Code_Symbol.Graph.map_node sym) (K stmt))
       |> pair deps
       |> pair x
   end;
 
 exception PERMISSIVE of unit;
 
 fun translation_error ctxt permissive some_thm deps msg sub_msg =
   if permissive
   then raise PERMISSIVE ()
   else
     let
       val thm_msg =
         Option.map (fn thm => "in code equation " ^ Thm.string_of_thm ctxt thm) some_thm;
       val dep_msg = if null (tl deps) then NONE
         else SOME ("with dependency "
           ^ space_implode " -> " (map (Code_Symbol.quote ctxt) (rev deps)));
       val thm_dep_msg = case (thm_msg, dep_msg)
        of (SOME thm_msg, SOME dep_msg) => "\n(" ^ thm_msg ^ ",\n" ^ dep_msg ^ ")"
         | (SOME thm_msg, NONE) => "\n(" ^ thm_msg ^ ")"
         | (NONE, SOME dep_msg) => "\n(" ^ dep_msg ^ ")"
         | (NONE, NONE) => ""
     in error (msg ^ thm_dep_msg ^ ":\n" ^ sub_msg) end;
 
 fun maybe_permissive f prgrm =
   f prgrm |>> SOME handle PERMISSIVE () => (NONE, prgrm);
 
 fun not_wellsorted ctxt permissive some_thm deps ty sort e =
   let
     val err_class = Sorts.class_error (Context.Proof ctxt) e;
     val err_typ =
       "Type " ^ Syntax.string_of_typ ctxt ty ^ " not of sort " ^
         Syntax.string_of_sort ctxt sort;
   in
     translation_error ctxt permissive some_thm deps
       "Wellsortedness error" (err_typ ^ "\n" ^ err_class)
   end;
 
 
 (* inference of type annotations for disambiguation with type classes *)
 
 fun mk_tagged_type (true, T) = Type ("", [T])
   | mk_tagged_type (false, T) = T;
 
 fun dest_tagged_type (Type ("", [T])) = (true, T)
   | dest_tagged_type T = (false, T);
 
 val untag_term = map_types (snd o dest_tagged_type);
 
 fun tag_term (proj_sort, _) eqngr =
   let
     val has_sort_constraints = exists (not o null) o map proj_sort o Code_Preproc.sortargs eqngr;
     fun tag (Const (_, T')) (Const (c, T)) =
         Const (c,
           mk_tagged_type (not (null (Term.add_tvarsT T' [])) andalso has_sort_constraints c, T))
       | tag (t1 $ u1) (t $ u) = tag t1 t $ tag u1 u
       | tag (Abs (_, _, t1)) (Abs (x, T, t)) = Abs (x, T, tag t1 t)
       | tag (Free _) (t as Free _) = t
       | tag (Var _) (t as Var _) = t
       | tag (Bound _) (t as Bound _) = t;
   in tag end
 
 fun annotate ctxt algbr eqngr (c, ty) args rhs =
   let
     val erase = map_types (fn _ => Type_Infer.anyT []);
     val reinfer = singleton (Type_Infer_Context.infer_types ctxt);
     val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o fst) args);
     val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))));
   in tag_term algbr eqngr reinferred_rhs rhs end
 
 fun annotate_eqns ctxt algbr eqngr (c, ty) eqns =
   let
     val ctxt' = ctxt |> Proof_Context.theory_of |> Proof_Context.init_global
       |> Config.put Type_Infer_Context.const_sorts false;
       (*avoid spurious fixed variables: there is no eigen context for equations*)
   in
     map (apfst (fn (args, (rhs, some_abs)) => (args,
       (annotate ctxt' algbr eqngr (c, ty) args rhs, some_abs)))) eqns
   end;
 
 (* abstract dictionary construction *)
 
 datatype typarg_witness =
     Weakening of (class * class) list * plain_typarg_witness
 and plain_typarg_witness =
     Global of (string * class) * typarg_witness list list
   | Local of { var: string, index: int, sort: sort, unique: bool };
 
 fun brand_unique unique (w as Global _) = w
   | brand_unique unique (Local { var, index, sort, unique = _ }) =
       Local { var = var, index = index, sort = sort, unique = unique };
 
 fun construct_dictionaries ctxt (proj_sort, algebra) permissive some_thm (ty, sort) (deps, program) =
   let
     fun class_relation unique (Weakening (classrels, x), sub_class) super_class =
       Weakening ((sub_class, super_class) :: classrels, brand_unique unique x);
     fun type_constructor (tyco, _) dss class =
       Weakening ([], Global ((tyco, class), (map o map) fst dss));
     fun type_variable (TFree (v, sort)) =
       let
         val sort' = proj_sort sort;
       in map_index (fn (n, class) => (Weakening ([], Local
         { var = v, index = n, sort = sort', unique = true }), class)) sort'
       end;
     val typarg_witnesses = Sorts.of_sort_derivation algebra
       {class_relation = fn _ => fn unique =>
          Sorts.classrel_derivation algebra (class_relation unique),
        type_constructor = type_constructor,
        type_variable = type_variable} (ty, proj_sort sort)
       handle Sorts.CLASS_ERROR e => not_wellsorted ctxt permissive some_thm deps ty sort e;
   in (typarg_witnesses, (deps, program)) end;
 
 
 (* translation *)
 
 fun ensure_tyco ctxt algbr eqngr permissive tyco =
   let
     val thy = Proof_Context.theory_of ctxt;
     val ((vs, cos), _) = Code.get_type thy tyco;
     val stmt_datatype =
       fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
       #>> map fst
       ##>> fold_map (fn (c, (vs, tys)) =>
         ensure_const ctxt algbr eqngr permissive c
         ##>> pair (map (unprefix "'" o fst) vs)
         ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys) cos
       #>> Datatype;
   in ensure_stmt Type_Constructor stmt_datatype tyco end
 and ensure_const ctxt algbr eqngr permissive c =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun stmt_datatypecons tyco =
       ensure_tyco ctxt algbr eqngr permissive tyco
       #>> Datatypecons;
     fun stmt_classparam class =
       ensure_class ctxt algbr eqngr permissive class
       #>> Classparam;
     fun stmt_fun cert = case Code.equations_of_cert thy cert
      of (_, NONE) => pair NoStmt
       | ((vs, ty), SOME eqns) =>
           let
             val eqns' = annotate_eqns ctxt algbr eqngr (c, ty) eqns
             val some_case_cong = Code.get_case_cong thy c;
           in
             fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
             ##>> translate_typ ctxt algbr eqngr permissive ty
             ##>> translate_eqns ctxt algbr eqngr permissive eqns'
             #>>
              (fn (_, NONE) => NoStmt
                | (tyscm, SOME eqns) => Fun ((tyscm, eqns), some_case_cong))
           end;
     val stmt_const = case Code.get_type_of_constr_or_abstr thy c
      of SOME (tyco, _) => stmt_datatypecons tyco
       | NONE => (case Axclass.class_of_param thy c
          of SOME class => stmt_classparam class
           | NONE => stmt_fun (Code_Preproc.cert eqngr c))
   in ensure_stmt Constant stmt_const c end
 and ensure_class ctxt (algbr as (_, algebra)) eqngr permissive class =
   let
     val thy = Proof_Context.theory_of ctxt;
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val cs = #params (Axclass.get_info thy class);
     val stmt_class =
       fold_map (fn super_class =>
         ensure_classrel ctxt algbr eqngr permissive (class, super_class)) super_classes
       ##>> fold_map (fn (c, ty) => ensure_const ctxt algbr eqngr permissive c
         ##>> translate_typ ctxt algbr eqngr permissive ty) cs
       #>> (fn info => Class (unprefix "'" Name.aT, info))
   in ensure_stmt Type_Class stmt_class class end
 and ensure_classrel ctxt algbr eqngr permissive (sub_class, super_class) =
   let
     val stmt_classrel =
       ensure_class ctxt algbr eqngr permissive sub_class
       ##>> ensure_class ctxt algbr eqngr permissive super_class
       #>> Classrel;
   in ensure_stmt Class_Relation stmt_classrel (sub_class, super_class) end
 and ensure_inst ctxt (algbr as (_, algebra)) eqngr permissive (tyco, class) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
     val these_class_params = these o try (#params o Axclass.get_info thy);
     val class_params = these_class_params class;
     val superclass_params = maps these_class_params
       ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
     val vs = Name.invent_names Name.context "'a" (Sorts.mg_domain algebra tyco [class]);
     val sorts' = Sorts.mg_domain (Sign.classes_of thy) tyco [class];
     val vs' = map2 (fn (v, sort1) => fn sort2 => (v,
       Sorts.inter_sort (Sign.classes_of thy) (sort1, sort2))) vs sorts';
     val arity_typ = Type (tyco, map TFree vs);
     val arity_typ' = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vs');
     fun translate_super_instance super_class =
       ensure_class ctxt algbr eqngr permissive super_class
       ##>> translate_dicts ctxt algbr eqngr permissive NONE (arity_typ, [super_class])
       #>> (fn (super_class, [Dict ([], Dict_Const (_, dss))]) => (super_class, dss));
     fun translate_classparam_instance (c, ty) =
       let
         val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
         val dom_length = length (fst (strip_type ty))
         val thm = Axclass.unoverload_conv ctxt (Thm.cterm_of ctxt raw_const);
         val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
           o Logic.dest_equals o Thm.prop_of) thm;
       in
         ensure_const ctxt algbr eqngr permissive c
         ##>> translate_const ctxt algbr eqngr permissive (SOME thm) (const, NONE)
         #>> (fn (c, IConst const') => ((c, (const', dom_length)), (thm, true)))
       end;
     val stmt_inst =
       ensure_class ctxt algbr eqngr permissive class
       ##>> ensure_tyco ctxt algbr eqngr permissive tyco
       ##>> fold_map (translate_tyvar_sort ctxt algbr eqngr permissive) vs
       ##>> fold_map translate_super_instance super_classes
       ##>> fold_map translate_classparam_instance class_params
       ##>> fold_map translate_classparam_instance superclass_params
       #>> (fn (((((class, tyco), vs), superinsts), inst_params), superinst_params) =>
           Classinst { class = class, tyco = tyco, vs = vs,
             superinsts = superinsts, inst_params = inst_params, superinst_params = superinst_params });
   in ensure_stmt Class_Instance stmt_inst (tyco, class) end
 and translate_typ ctxt algbr eqngr permissive (TFree (v, _)) =
       pair (ITyVar (unprefix "'" v))
   | translate_typ ctxt algbr eqngr permissive (Type (tyco, tys)) =
       ensure_tyco ctxt algbr eqngr permissive tyco
       ##>> fold_map (translate_typ ctxt algbr eqngr permissive) tys
       #>> (fn (tyco, tys) => tyco `%% tys)
 and translate_term ctxt algbr eqngr permissive some_thm (Const (c, ty), some_abs) =
       translate_app ctxt algbr eqngr permissive some_thm (((c, ty), []), some_abs)
   | translate_term ctxt algbr eqngr permissive some_thm (Free (v, _), some_abs) =
       pair (IVar (SOME v))
   | translate_term ctxt algbr eqngr permissive some_thm (Abs (v, ty, t), some_abs) =
       let
-        val (v', t') = Syntax_Trans.variant_abs (Name.desymbolize (SOME false) v, ty, t);
-        val v'' = if member (op =) (Term.add_free_names t' []) v'
-          then SOME v' else NONE
+        val (v', t') = Term.dest_abs (Name.desymbolize (SOME false) v, ty, t);
+        val v'' = if Term.used_free v' t' then SOME v' else NONE
       in
         translate_typ ctxt algbr eqngr permissive ty
         ##>> translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
         #>> (fn (ty, t) => (v'', ty) `|=> t)
       end
   | translate_term ctxt algbr eqngr permissive some_thm (t as _ $ _, some_abs) =
       case strip_comb t
        of (Const (c, ty), ts) =>
             translate_app ctxt algbr eqngr permissive some_thm (((c, ty), ts), some_abs)
         | (t', ts) =>
             translate_term ctxt algbr eqngr permissive some_thm (t', some_abs)
             ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
             #>> (fn (t, ts) => t `$$ ts)
 and translate_eqn ctxt algbr eqngr permissive ((args, (rhs, some_abs)), (some_thm, proper)) =
   fold_map (translate_term ctxt algbr eqngr permissive some_thm) args
   ##>> translate_term ctxt algbr eqngr permissive some_thm (rhs, some_abs)
   #>> rpair (some_thm, proper)
 and translate_eqns ctxt algbr eqngr permissive eqns =
   maybe_permissive (fold_map (translate_eqn ctxt algbr eqngr permissive) eqns)
 and translate_const ctxt algbr eqngr permissive some_thm ((c, ty), some_abs) (deps, program) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
         andalso Code.is_abstr thy c
         then translation_error ctxt permissive some_thm deps
           "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
       else ()
   in translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) (deps, program) end
 and translate_const_proper ctxt algbr eqngr permissive some_thm (c, ty) =
   let
     val thy = Proof_Context.theory_of ctxt;
     val (annotate, ty') = dest_tagged_type ty;
     val typargs = Sign.const_typargs thy (c, ty');
     val sorts = Code_Preproc.sortargs eqngr c;
     val (dom, range) = Term.strip_type ty';
   in
     ensure_const ctxt algbr eqngr permissive c
     ##>> fold_map (translate_typ ctxt algbr eqngr permissive) typargs
     ##>> fold_map (translate_dicts ctxt algbr eqngr permissive some_thm) (typargs ~~ sorts)
     ##>> fold_map (translate_typ ctxt algbr eqngr permissive) (ty' :: dom)
     #>> (fn (((c, typargs), dss), annotation :: dom) =>
       IConst { sym = Constant c, typargs = typargs, dicts = dss,
         dom = dom, annotation =
           if annotate then SOME annotation else NONE })
   end
 and translate_app_const ctxt algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
   translate_const ctxt algbr eqngr permissive some_thm (c_ty, some_abs)
   ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
   #>> (fn (t, ts) => t `$$ ts)
 and translate_case ctxt algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun arg_types num_args ty = fst (chop num_args (binder_types ty));
     val tys = arg_types num_args (snd c_ty);
     val ty = nth tys t_pos;
     fun mk_constr NONE t = NONE
       | mk_constr (SOME c) t =
           let
             val n = Code.args_number thy c;
           in SOME ((c, arg_types n (fastype_of (untag_term t)) ---> ty), n) end;
     val constrs =
       if null case_pats then []
       else map_filter I (map2 mk_constr case_pats (nth_drop t_pos ts));
     fun disjunctive_varnames ts =
       let
         val vs = (fold o fold_varnames) (insert (op =)) ts [];
       in fn pat => null (inter (op =) vs (fold_varnames (insert (op =)) pat [])) end;
     fun purge_unused_vars_in t =
       let
         val vs = fold_varnames (insert (op =)) t [];
       in
         map_terms_bottom_up (fn IVar (SOME v) =>
           IVar (if member (op =) vs v then SOME v else NONE) | t => t)
       end;
     fun collapse_clause vs_map ts body =
       case body
        of IConst { sym = Constant c, ... } => if Code.is_undefined thy c
             then []
             else [(ts, body)]
         | ICase { term = IVar (SOME v), clauses = clauses, ... } =>
             if forall (fn (pat', body') => exists_var pat' v
               orelse not (exists_var body' v)) clauses
               andalso forall (disjunctive_varnames ts o fst) clauses
             then case AList.lookup (op =) vs_map v
              of SOME i => maps (fn (pat', body') =>
                   collapse_clause (AList.delete (op =) v vs_map)
                     (nth_map i (K pat') ts |> map (purge_unused_vars_in body')) body') clauses
               | NONE => [(ts, body)]
             else [(ts, body)]
         | _ => [(ts, body)];
     fun mk_clause mk tys t =
       let
         val (vs, body) = unfold_abs_eta tys t;
         val vs_map = fold_index (fn (i, (SOME v, _)) => cons (v, i) | _ => I) vs [];
         val ts = map (IVar o fst) vs;
       in map mk (collapse_clause vs_map ts body) end;
     fun casify constrs ty t_app ts =
       let
         val t = nth ts t_pos;
         val ts_clause = nth_drop t_pos ts;
         val clauses = if null case_pats
           then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
           else maps (fn ((constr as IConst { dom = tys, ... }, n), t) =>
             mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
               (constrs ~~ (map_filter (fn (NONE, _) => NONE | (SOME _, t) => SOME t)
                 (case_pats ~~ ts_clause)));
       in ICase { term = t, typ = ty, clauses = clauses, primitive = t_app `$$ ts } end;
   in
     translate_const ctxt algbr eqngr permissive some_thm (c_ty, NONE)
     ##>> fold_map (fn (constr, n) => translate_const ctxt algbr eqngr permissive some_thm (constr, NONE)
       #>> rpair n) constrs
     ##>> translate_typ ctxt algbr eqngr permissive ty
     ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) ts
     #>> (fn (((t, constrs), ty), ts) =>
       casify constrs ty t ts)
   end
 and translate_app_case ctxt algbr eqngr permissive some_thm (case_schema as (num_args, _)) ((c, ty), ts) =
   if length ts < num_args then
     let
       val k = length ts;
       val tys = (take (num_args - k) o drop k o fst o strip_type) ty;
       val names = Name.build_context (ts |> (fold o fold_aterms) Term.declare_term_frees);
       val vs = Name.invent_names names "a" tys;
     in
       fold_map (translate_typ ctxt algbr eqngr permissive) tys
       ##>> translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), ts @ map Free vs)
       #>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
     end
   else if length ts > num_args then
     translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), take num_args ts)
     ##>> fold_map (translate_term ctxt algbr eqngr permissive some_thm o rpair NONE) (drop num_args ts)
     #>> (fn (t, ts) => t `$$ ts)
   else
     translate_case ctxt algbr eqngr permissive some_thm case_schema ((c, ty), ts)
 and translate_app ctxt algbr eqngr permissive some_thm (c_ty_ts as ((c, _), _), some_abs) =
   case Code.get_case_schema (Proof_Context.theory_of ctxt) c
    of SOME case_schema => translate_app_case ctxt algbr eqngr permissive some_thm case_schema c_ty_ts
     | NONE => translate_app_const ctxt algbr eqngr permissive some_thm (c_ty_ts, some_abs)
 and translate_tyvar_sort ctxt (algbr as (proj_sort, _)) eqngr permissive (v, sort) =
   fold_map (ensure_class ctxt algbr eqngr permissive) (proj_sort sort)
   #>> (fn sort => (unprefix "'" v, sort))
 and translate_dicts ctxt algbr eqngr permissive some_thm (ty, sort) =
   let
     fun mk_dict (Weakening (classrels, d)) =
           fold_map (ensure_classrel ctxt algbr eqngr permissive) classrels
           ##>> mk_plain_dict d
           #>> Dict 
     and mk_plain_dict (Global (inst, dss)) =
           ensure_inst ctxt algbr eqngr permissive inst
           ##>> (fold_map o fold_map) mk_dict dss
           #>> Dict_Const
       | mk_plain_dict (Local { var, index, sort, unique }) =
           ensure_class ctxt algbr eqngr permissive (nth sort index)
           #>> (fn class => Dict_Var { var = unprefix "'" var, index = index,
             length = length sort, class = class, unique = unique })
   in
     construct_dictionaries ctxt algbr permissive some_thm (ty, sort)
     #-> (fn typarg_witnesses => fold_map mk_dict typarg_witnesses)
   end;
 
 
 (* store *)
 
 structure Program = Code_Data
 (
   type T = program;
   val empty = Code_Symbol.Graph.empty;
 );
 
 fun invoke_generation ignore_cache ctxt generate thing =
   Program.change_yield
     (if ignore_cache then NONE else SOME (Proof_Context.theory_of ctxt))
     (fn program => ([], program)
       |> generate thing
       |-> (fn thing => fn (_, program) => (thing, program)));
 
 
 (* program generation *)
 
 fun check_abstract_constructors thy consts =
   case filter (Code.is_abstr thy) consts of
     [] => ()
   | abstrs => error ("Cannot export abstract constructor(s): "
       ^ commas (map (Code.string_of_const thy) abstrs));
 
 fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts =
   let
     val thy = Proof_Context.theory_of ctxt;
     val _ = if permissive then ()
       else check_abstract_constructors thy consts;
   in
     Code_Preproc.timed "translating program" #ctxt
     (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt
       (fold_map (ensure_const ctxt algebra eqngr permissive)) consts)
       { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }
   end;
 
 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts =
   invoke_generation_for_consts ctxt
     { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive }
     (Code_Preproc.obtain ignore_cache_and_permissive
       { ctxt = ctxt, consts = consts, terms = []}) consts
   |> snd;
 
 fun invoke_generation_for_consts'' ctxt algebra_eqngr =
   invoke_generation_for_consts ctxt
     { ignore_cache = true, permissive = false }
     algebra_eqngr
   #> (fn (deps, program) => { deps = deps, program = program });
 
 fun consts_program_permissive ctxt =
   invoke_generation_for_consts' ctxt true;
 
 fun consts_program ctxt consts =
   let
     fun project program = Code_Symbol.Graph.restrict
       (member (op =) (Code_Symbol.Graph.all_succs program
         (map Constant consts))) program;
   in
     invoke_generation_for_consts' ctxt false consts
     |> project
   end;
 
 
 (* value evaluation *)
 
 fun ensure_value ctxt algbr eqngr t =
   let
     val ty = fastype_of t;
     val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
       o dest_TFree))) t [];
     val t' = annotate ctxt algbr eqngr (\<^const_name>\<open>Pure.dummy_pattern\<close>, ty) [] t;
     val dummy_constant = Constant \<^const_name>\<open>Pure.dummy_pattern\<close>;
     val stmt_value =
       fold_map (translate_tyvar_sort ctxt algbr eqngr false) vs
       ##>> translate_typ ctxt algbr eqngr false ty
       ##>> translate_term ctxt algbr eqngr false NONE (t', NONE)
       #>> (fn ((vs, ty), t) => Fun
         (((vs, ty), [(([], t), (NONE, true))]), NONE));
     fun term_value (_, program1) =
       let
         val Fun ((vs_ty, [(([], t), _)]), _) =
           Code_Symbol.Graph.get_node program1 dummy_constant;
         val deps' = Code_Symbol.Graph.immediate_succs program1 dummy_constant;
         val program2 = Code_Symbol.Graph.del_node dummy_constant program1;
         val deps_all = Code_Symbol.Graph.all_succs program2 deps';
         val program3 = Code_Symbol.Graph.restrict (member (op =) deps_all) program2;
        in ((program3, ((vs_ty, t), deps')), (deps', program2)) end;
   in
     ensure_stmt Constant stmt_value \<^const_name>\<open>Pure.dummy_pattern\<close>
     #> snd
     #> term_value
   end;
 
 fun dynamic_evaluation comp ctxt algebra eqngr t =
   let
     val ((program, (vs_ty_t', deps)), _) =
       Code_Preproc.timed "translating term" #ctxt
       (fn { ctxt, algebra, eqngr, t } =>
         invoke_generation false ctxt (ensure_value ctxt algebra eqngr) t)
         { ctxt = ctxt, algebra = algebra, eqngr = eqngr, t = t };
   in comp program t vs_ty_t' deps end;
 
 fun dynamic_conv ctxt conv =
   Code_Preproc.dynamic_conv ctxt
     (dynamic_evaluation (fn program => fn _ => conv program) ctxt);
 
 fun dynamic_value ctxt postproc comp =
   Code_Preproc.dynamic_value ctxt postproc
     (dynamic_evaluation comp ctxt);
 
 fun static_evaluation ctxt consts algebra_eqngr static_eval =
   static_eval (invoke_generation_for_consts'' ctxt algebra_eqngr consts);
 
 fun static_evaluation_thingol ctxt consts (algebra_eqngr as { algebra, eqngr }) static_eval =
   let
     fun evaluation program dynamic_eval ctxt t =
       let
         val ((_, ((vs_ty', t'), deps)), _) =
           Code_Preproc.timed "translating term" #ctxt
           (fn { ctxt, t } =>
             ensure_value ctxt algebra eqngr t ([], program))
             { ctxt = ctxt, t = t };
       in dynamic_eval ctxt t (vs_ty', t') deps end;
   in
     static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
       evaluation (#program program_deps) (static_eval program_deps))
   end;
 
 fun static_evaluation_isa ctxt consts algebra_eqngr static_eval =
   static_evaluation ctxt consts algebra_eqngr (fn program_deps =>
     (static_eval (#program program_deps)));
 
 fun static_conv_thingol (ctxt_consts as { ctxt, consts }) conv =
   Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr =>
     static_evaluation_thingol ctxt consts algebra_eqngr
       (fn program_deps =>
         let
           val static_conv = conv program_deps;
         in 
           fn ctxt => fn _ => fn vs_ty => fn deps => static_conv ctxt vs_ty deps
         end));
 
 fun static_conv_isa (ctxt_consts as { ctxt, consts }) conv =
   Code_Preproc.static_conv ctxt_consts (fn algebra_eqngr =>
     static_evaluation_isa ctxt consts algebra_eqngr conv);
 
 fun static_value (ctxt_postproc_consts as { ctxt, consts, ... }) comp =
   Code_Preproc.static_value ctxt_postproc_consts (fn algebra_eqngr =>
     static_evaluation_thingol ctxt consts algebra_eqngr comp);
 
 
 (** constant expressions **)
 
 fun read_const_exprs_internal ctxt =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun this_theory name =
       if Context.theory_name thy = name then thy
       else Context.get_theory {long = false} thy name;
 
     fun consts_of thy' =
       fold (fn (c, (_, NONE)) => cons c | _ => I)
         (#constants (Consts.dest (Sign.consts_of thy'))) []
       |> filter_out (Code.is_abstr thy);
     fun belongs_here thy' c = forall
       (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy');
     fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
     fun read_const_expr str =
       (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of
         SOME "_" => ([], consts_of thy)
       | SOME s =>
           (case try (unsuffix "._") s of
             SOME name => ([], consts_of_select (this_theory name))
           | NONE => ([Code.read_const thy str], []))
       | NONE => ([Code.read_const thy str], []));
   in apply2 flat o split_list o map read_const_expr end;
 
 fun read_const_exprs_all ctxt = op @ o read_const_exprs_internal ctxt;
 
 fun read_const_exprs ctxt const_exprs =
   let
     val (consts, consts_permissive) =
       read_const_exprs_internal ctxt const_exprs;
     val consts' = 
       consts_program_permissive ctxt consts_permissive
       |> implemented_deps
       |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt));
   in union (op =) consts' consts end;
 
 
 (** diagnostic commands **)
 
 fun code_depgr ctxt consts =
   let
     val { eqngr, ... } = Code_Preproc.obtain true
       { ctxt = ctxt, consts = consts, terms = [] };
     val all_consts = Graph.all_succs eqngr consts;
   in Graph.restrict (member (op =) all_consts) eqngr end;
 
 fun code_thms ctxt = Pretty.writeln o Code_Preproc.pretty ctxt o code_depgr ctxt;
 
 fun coalesce_strong_conn gr =
   let
     val xss = Graph.strong_conn gr;
     val xss_ys = map (fn xs => (xs, commas xs)) xss;
     val y_for = the o AList.lookup (op =) (maps (fn (xs, y) => map (fn x => (x, y)) xs) xss_ys);
     fun coalesced_succs_for xs = maps (Graph.immediate_succs gr) xs
       |> subtract (op =) xs
       |> map y_for
       |> distinct (op =);
     val succs = map (fn (xs, _) => (xs, coalesced_succs_for xs)) xss_ys;
   in
     map (fn (xs, y) => ((y, xs), (maps (Graph.get_node gr) xs, (the o AList.lookup (op =) succs) xs))) xss_ys
   end;
 
 fun code_deps ctxt consts =
   let
     val thy = Proof_Context.theory_of ctxt;
     fun mk_entry ((name, consts), (ps, deps)) =
       let
         val label = commas (map (Code.string_of_const thy) consts);
       in ((name, Graph_Display.content_node label (Pretty.str label :: ps)), deps) end;
   in
     code_depgr ctxt consts
     |> Graph.map (K (Code.pretty_cert thy o snd))
     |> coalesce_strong_conn
     |> map mk_entry
     |> Graph_Display.display_graph
   end;
 
 local
 
 fun code_thms_cmd ctxt = code_thms ctxt o read_const_exprs_all ctxt;
 fun code_deps_cmd ctxt = code_deps ctxt o read_const_exprs_all ctxt;
 
 in
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_thms\<close>
     "print system of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>code_deps\<close>
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
       Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
 
 end;
 
 end; (*struct*)
 
 
 structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;