# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259286354 -3600
# Node ID 1056861b562c7b45218c8be9b3d06dd8d5508b26
# Parent  d387743f022bd1de1449306e9288f6cb00d2104f
renamed inj_REPABS to inj_repabs_trm

diff -r d387743f022b -r 1056861b562c QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 02:44:11 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 02:45:54 2009 +0100
@@ -637,24 +637,24 @@
 (* bound variables need to be treated properly,  *)
 (* as the type of subterms need to be calculated *)
 
-fun inj_REPABS lthy (rtrm, qtrm) =
+fun inj_repabs_trm lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
   val qty = fastype_of qtrm
 in
   case (rtrm, qtrm) of
     (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-       Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
+       Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-       Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
+       Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
   | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
-       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
+       Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm lthy (t, t'))
   | (Abs (x, T, t), Abs (x', T', t')) =>
       let
         val (y, s) = Term.dest_abs (x, T, t)
         val (_, s') = Term.dest_abs (x', T', t')
         val yvar = Free (y, T)
-        val result = lambda yvar (inj_REPABS lthy (s, s'))
+        val result = lambda yvar (inj_repabs_trm lthy (s, s'))
       in
         if rty = qty 
         then result
@@ -668,7 +668,7 @@
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
-        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
+        val rargs' = map (inj_repabs_trm lthy) (rargs ~~ qargs)
       in
         if rty = qty
         then
@@ -685,7 +685,7 @@
           | (Free (x, T), Free (x', T'), _) => 
                mk_repabs lthy (rty, qty) (list_comb (mk_repabs lthy (T, T') rhead, rargs'))
           | (Abs _, Abs _, _ ) =>
-               mk_repabs lthy (rty, qty) (list_comb (inj_REPABS lthy (rhead, qhead), rargs')) 
+               mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
           | _ => raise (LIFT_MATCH "injection")
       end
 end
@@ -1123,7 +1123,7 @@
         Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm')
         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
   val inj_goal = 
-        Syntax.check_term ctxt (inj_REPABS ctxt (reg_goal, qtrm'))
+        Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm'))
         handle (LIFT_MATCH s) => lift_error ctxt s rtrm qtrm
 in
   Drule.instantiate' []