--- a/Quot/quotient_term.ML	Wed Jan 27 08:20:31 2010 +0100
+++ b/Quot/quotient_term.ML	Wed Jan 27 08:41:42 2010 +0100
@@ -1,11 +1,16 @@
+(*  Title:      quotient_term.thy
+    Author:     Cezary Kaliszyk and Christian Urban
+
+    Constructs terms corresponding to goals from
+    lifting theorems to quotient types.
+*)
+
 signature QUOTIENT_TERM =
 sig
   exception LIFT_MATCH of string
 
   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
 
@@ -128,9 +133,6 @@
   | 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
@@ -434,13 +436,14 @@
          else mk_ball $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "All"}, ty') $ t') =>
+  | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "All"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(ball)" ctxt resrel needrel
+         then term_mismatch "regularize (Ball)" ctxt resrel needrel
          else mk_ball $ (mk_resp $ resrel) $ subtrm
        end
 
@@ -452,13 +455,14 @@
          else mk_bex $ (mk_resp $ equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
        end
 
-  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
+  | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "Ex"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex)" ctxt resrel needrel
          else mk_bex $ (mk_resp $ resrel) $ subtrm
        end
 
@@ -473,20 +477,21 @@
   | (Const (@{const_name "Bexeq"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex1_res)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex1_res)" ctxt resrel needrel
          else mk_bexeq $ resrel $ subtrm
        end
 
-  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
+  | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, 
+     Const (@{const_name "Ex1"}, ty') $ t') =>
        let
          val subtrm = apply_subt (regularize_trm ctxt) (t, t')
-         val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty'))
+         val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
        in
          if resrel <> needrel
-         then term_mismatch "regularize(bex1)" ctxt resrel needrel
+         then term_mismatch "regularize (Bex1)" ctxt resrel needrel
          else mk_bexeq $ resrel $ subtrm
        end
 
@@ -501,7 +506,8 @@
          val rel_ty = fastype_of rel
          val rel' = equiv_relation_chk ctxt (domain_type rel_ty, domain_type ty') 
        in
-         if rel' aconv rel then rtrm else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
+         if rel' aconv rel then rtrm 
+         else term_mismatch "regularise (relation mismatch)" ctxt rel rel'
        end
 
   | (_, Const _) =>