--- a/Quot/Examples/LamEx.thy	Thu Jan 14 15:36:29 2010 +0100
+++ b/Quot/Examples/LamEx.thy	Thu Jan 14 16:41:17 2010 +0100
@@ -242,11 +242,24 @@
   by (lifting rvar_inject)
 
 lemma lam_induct:
-  "\<lbrakk>\<And>name. P (Var name); 
+  "\<lbrakk>\<And>name. P (Var name);
     \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
     \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
   by (lifting rlam.induct)
 
+lemma lam_induct_strong_pre:
+  "\<lbrakk>\<And>name b. P b (Var name);
+    \<And>lam1 lam2 b. \<lbrakk>\<And>c. P c lam1; \<And>c. P c lam2\<rbrakk> \<Longrightarrow> P b (App lam1 lam2);
+    \<And>name lam b. \<lbrakk>\<And>c. P c lam; name \<sharp> (c \<bullet> lam)\<rbrakk> \<Longrightarrow> P b (Lam name lam)\<rbrakk> \<Longrightarrow> P a lam"
+sorry
+
+lemma lam_induct_strong:
+  "\<lbrakk>\<And>name. P (Var name);
+    \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
+    \<And>name lam. P lam \<Longrightarrow> name \<sharp> lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
+sorry
+
+
 lemma var_supp:
   shows "supp (Var a) = ((supp a)::name set)"
   apply(simp add: supp_def)

--- a/Quot/quotient_term.ML	Thu Jan 14 15:36:29 2010 +0100
+++ b/Quot/quotient_term.ML	Thu Jan 14 16:41:17 2010 +0100
@@ -4,6 +4,8 @@
 
   datatype flag = absF | repF
 
+  val absrep_const_chk: flag -> Proof.context -> string -> term
+
   val absrep_fun: flag -> Proof.context -> typ * typ -> term
   val absrep_fun_chk: flag -> Proof.context -> typ * typ -> term
 
@@ -126,6 +128,9 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
+fun absrep_const_chk flag ctxt qty_str =
+  Syntax.check_term ctxt (absrep_const flag ctxt qty_str)
+
 fun absrep_match_err ctxt ty_pat ty =
 let
   val ty_pat_str = Syntax.string_of_typ ctxt ty_pat