--- a/IntEx.thy	Thu Nov 26 21:16:59 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 02:23:49 2009 +0100
@@ -174,7 +174,7 @@
 *)
 
 ML {*
-  mk_REGULARIZE_goal @{context} 
+  mk_regularize_trm @{context} 
     @{term "\<forall>i j k. my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"}
     @{term "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"}
   |> Syntax.string_of_term @{context}

--- a/QuotMain.thy	Thu Nov 26 21:16:59 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 02:23:49 2009 +0100
@@ -381,7 +381,7 @@
 ML {*
 (* - applies f to the subterm of an abstraction,   *)
 (*   otherwise to the given term,                  *)
-(* - used by REGULARIZE, therefore abstracted      *)
+(* - used by regularize, therefore abstracted      *)
 (*   variables do not have to be treated specially *)
 
 fun apply_subt f trm1 trm2 =
@@ -399,11 +399,11 @@
 (* - does not need any special treatment of   *)
 (*   bound variables                          *)
 
-fun REGULARIZE_trm lthy rtrm qtrm =
+fun regularize_trm lthy rtrm qtrm =
   case (rtrm, qtrm) of
     (Abs (x, ty, t), Abs (x', ty', t')) =>
        let
-         val subtrm = REGULARIZE_trm lthy t t'
+         val subtrm = regularize_trm lthy t t'
        in     
          if ty = ty'
          then Abs (x, ty, subtrm)
@@ -411,7 +411,7 @@
        end
   | (Const (@{const_name "All"}, ty) $ t, Const (@{const_name "All"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+         val subtrm = apply_subt (regularize_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "All"}, ty) $ subtrm
@@ -419,7 +419,7 @@
        end
   | (Const (@{const_name "Ex"}, ty) $ t, Const (@{const_name "Ex"}, ty') $ t') =>
        let
-         val subtrm = apply_subt (REGULARIZE_trm lthy) t t'
+         val subtrm = apply_subt (regularize_trm lthy) t t'
        in
          if ty = ty'
          then Const (@{const_name "Ex"}, ty) $ subtrm
@@ -429,14 +429,14 @@
     (* Then there must be a 2nd argument                     *)
   | (Const (@{const_name "op ="}, ty) $ t, Const (@{const_name "op ="}, ty') $ t') =>
        let
-         val subtrm = REGULARIZE_trm lthy t t'
+         val subtrm = regularize_trm lthy t t'
        in
          if ty = ty'
          then Const (@{const_name "op ="}, ty) $ subtrm
          else mk_resp_arg lthy (domain_type ty, domain_type ty') $ subtrm
        end 
   | (t1 $ t2, t1' $ t2') =>
-       (REGULARIZE_trm lthy t1 t1') $ (REGULARIZE_trm lthy t2 t2')
+       (regularize_trm lthy t1 t1') $ (regularize_trm lthy t2 t2')
   | (Free (x, ty), Free (x', ty')) =>
        if x = x' 
        then rtrm     (* FIXME: check whether types corresponds *)
@@ -477,7 +477,7 @@
   shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)"
 using a b by auto
 
-(* version of REGULARIZE_tac including debugging information *)
+(* version of regularize_tac including debugging information *)
 ML {*
 fun my_print_tac ctxt s thm =
 let
@@ -1115,7 +1115,7 @@
   val rtrm' = HOLogic.dest_Trueprop rtrm
   val qtrm' = HOLogic.dest_Trueprop qtrm
   val reg_goal = 
-        Syntax.check_term ctxt (REGULARIZE_trm ctxt rtrm' qtrm')
+        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'))