--- a/Quot/Examples/FSet.thy	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/Examples/FSet.thy	Tue Dec 22 21:31:44 2009 +0100
@@ -43,7 +43,7 @@
 *}
 
 ML {*
-get_fun absF @{context} (@{typ "'a list"}, 
+absrep_fun absF @{context} (@{typ "'a list"}, 
                          @{typ "'a fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -54,7 +54,7 @@
 term "abs_fset o (map id)"
 
 ML {*
-get_fun absF @{context} (@{typ "(nat * nat) list"}, 
+absrep_fun absF @{context} (@{typ "(nat * nat) list"}, 
                          @{typ "int fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -66,7 +66,7 @@
 
 
 ML {*
-get_fun absF @{context} (@{typ "('a list) list"}, 
+absrep_fun absF @{context} (@{typ "('a list) list"}, 
                          @{typ "('a fset) fset"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}
@@ -74,7 +74,7 @@
 *}
 
 ML {*
-get_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
+absrep_fun absF @{context} (@{typ "('a list) list \<Rightarrow> 'a"}, 
                          @{typ "('a fset) fset \<Rightarrow> 'a"})
 |> Syntax.check_term @{context}
 |> Syntax.string_of_term @{context}

--- a/Quot/quotient_def.ML	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/quotient_def.ML	Tue Dec 22 21:31:44 2009 +0100
@@ -36,8 +36,7 @@
 let
   val Free (lhs_str, lhs_ty) = lhs;
   val qconst_bname = Binding.name lhs_str;
-  val absrep_trm = get_fun absF lthy (fastype_of rhs, lhs_ty) $ rhs
-                   |> Syntax.check_term lthy
+  val absrep_trm = absrep_fun_chk absF lthy (fastype_of rhs, lhs_ty) $ rhs
   val prop = Logic.mk_equals (lhs, absrep_trm)
   val (_, prop') = LocalDefs.cert_def lthy prop
   val (_, newrhs) = Primitive_Defs.abs_def prop'

--- a/Quot/quotient_tacs.ML	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/quotient_tacs.ML	Tue Dec 22 21:31:44 2009 +0100
@@ -586,11 +586,9 @@
   val thy = ProofContext.theory_of ctxt
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
-  val reg_goal = 
-        Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm'))
+  val reg_goal = regularize_trm_chk ctxt (rtrm', qtrm')
         handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
-  val inj_goal = 
-        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
+  val inj_goal = inj_repabs_trm_chk ctxt (reg_goal, qtrm')
         handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm
 in
   Drule.instantiate' []

--- a/Quot/quotient_term.ML	Tue Dec 22 21:16:11 2009 +0100
+++ b/Quot/quotient_term.ML	Tue Dec 22 21:31:44 2009 +0100
@@ -3,10 +3,15 @@
    exception LIFT_MATCH of string
  
    datatype flag = absF | repF
-   val get_fun: flag -> Proof.context -> (typ * typ) -> term
+   
+   val absrep_fun: flag -> Proof.context -> (typ * typ) -> term
+   val absrep_fun_chk: flag -> Proof.context -> (typ * typ) -> term
 
    val regularize_trm: Proof.context -> (term * term) -> term
+   val regularize_trm_chk: Proof.context -> (term * term) -> term
+   
    val inj_repabs_trm: Proof.context -> (term * term) -> term
+   val inj_repabs_trm_chk: Proof.context -> (term * term) -> term
 end;
 
 structure Quotient_Term: QUOTIENT_TERM =
@@ -33,10 +38,10 @@
     absF => Const (@{const_name "comp"}, dummyT) $ trm1 $ trm2
   | repF => Const (@{const_name "comp"}, dummyT) $ trm2 $ trm1
 
-fun get_fun_aux lthy s fs =
+fun absrep_fun_aux lthy s fs =
 let
   val thy = ProofContext.theory_of lthy
-  val exc = LIFT_MATCH (space_implode " " ["get_fun_aux: no map for type", quote s, "."])
+  val exc = LIFT_MATCH (space_implode " " ["absrep_fun_aux: no map for type", quote s, "."])
   val info = maps_lookup thy s handle NotFound => raise exc
 in
   list_comb (Const (#mapfun info, dummyT), fs)
@@ -53,15 +58,15 @@
   | repF => Const (Sign.full_bname thy ("rep_" ^ qty_name), dummyT)
 end
 
-fun get_fun flag lthy (rty, qty) =
+fun absrep_fun flag lthy (rty, qty) =
   if rty = qty then mk_identity qty else
   case (rty, qty) of
     (Type ("fun", [ty1, ty2]), Type ("fun", [ty1', ty2'])) =>
      let
-       val fs_ty1 = get_fun (negF flag) lthy (ty1, ty1')
-       val fs_ty2 = get_fun flag lthy (ty2, ty2')
+       val fs_ty1 = absrep_fun (negF flag) lthy (ty1, ty1')
+       val fs_ty2 = absrep_fun flag lthy (ty2, ty2')
      in
-       get_fun_aux lthy "fun" [fs_ty1, fs_ty2]
+       absrep_fun_aux lthy "fun" [fs_ty1, fs_ty2]
      end
   | (Type (s, _), Type (s', [])) =>
      if s = s'
@@ -69,19 +74,22 @@
      else get_const flag lthy rty qty
   | (Type (s, tys), Type (s', tys')) =>
      let
-        val args = map (get_fun flag lthy) (tys ~~ tys')
+        val args = map (absrep_fun flag lthy) (tys ~~ tys')
      in
         if s = s'
-        then get_fun_aux lthy s args
-        else mk_compose flag (get_const flag lthy rty qty, get_fun_aux lthy s args)
+        then absrep_fun_aux lthy s args
+        else mk_compose flag (get_const flag lthy rty qty, absrep_fun_aux lthy s args)
      end
   | (TFree x, TFree x') =>
      if x = x'
      then mk_identity qty
-     else raise (LIFT_MATCH "get_fun (frees)")
-  | (TVar _, TVar _) => raise (LIFT_MATCH "get_fun (vars)")
-  | _ => raise (LIFT_MATCH "get_fun (default)")
+     else raise (LIFT_MATCH "absrep_fun (frees)")
+  | (TVar _, TVar _) => raise (LIFT_MATCH "absrep_fun (vars)")
+  | _ => raise (LIFT_MATCH "absrep_fun (default)")
 
+fun absrep_fun_chk flag lthy (rty, qty) =
+  absrep_fun flag lthy (rty, qty)
+  |> Syntax.check_term lthy
 
 (*
 Regularizing an rtrm means:
@@ -259,7 +267,9 @@
          raise (LIFT_MATCH ("regularize failed (default: " ^ rtrm_str ^ "," ^ qtrm_str ^ ")"))
        end
 
-
+fun regularize_trm_chk lthy (rtrm, qtrm) =
+  regularize_trm lthy (rtrm, qtrm) 
+  |> Syntax.check_term lthy
 
 (*
 Injection of Rep/Abs means:
@@ -290,7 +300,7 @@
 *)
 
 fun mk_repabs lthy (T, T') trm = 
-  get_fun repF lthy (T, T') $ (get_fun absF lthy (T, T') $ trm)
+  absrep_fun repF lthy (T, T') $ (absrep_fun absF lthy (T, T') $ trm)
 
 
 (* bound variables need to be treated properly,     *)
@@ -344,6 +354,10 @@
   
   | _ => raise (LIFT_MATCH "injection (default)")
 
+fun inj_repabs_trm_chk lthy (rtrm, qtrm) =
+  inj_repabs_trm lthy (rtrm, qtrm) 
+  |> Syntax.check_term lthy
+
 end; (* structure *)