diff -r 6f3771c00280 -r 47d138cae708 src/HOL/Tools/reflection.ML
--- a/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
+++ b/src/HOL/Tools/reflection.ML	Fri May 31 09:30:32 2013 +0200
@@ -6,9 +6,11 @@
 
 signature REFLECTION =
 sig
-  val gen_reify: Proof.context -> thm list -> term -> thm
-  val gen_reify_tac: Proof.context -> thm list -> term option -> int -> tactic
-  val gen_reflection_tac: Proof.context -> (cterm -> thm)
+  val reify: Proof.context -> thm list -> term -> thm
+  val reify_tac: Proof.context -> thm list -> term option -> int -> tactic
+  val reflect: Proof.context -> (cterm -> thm)
+    -> thm list -> thm list -> term -> thm
+  val reflection_tac: Proof.context -> (cterm -> thm)
     -> thm list -> thm list -> term option -> int -> tactic
   val get_default: Proof.context -> { reification_eqs: thm list, correctness_thms: thm list }
   val add_reification_eq: attribute
@@ -94,7 +96,7 @@
     val (yes, no) = List.partition P congs;
   in no @ yes end;
 
-fun gen_reify ctxt eqs t =
+fun reify ctxt eqs t =
   let
     fun index_of t bds =
       let
@@ -124,7 +126,7 @@
     (* da is the decomposition for atoms, ie. it returns ([],g) where g
        returns the right instance f (AtC n) = t , where AtC is the Atoms
        constructor and n is the number of the atom corresponding to t *)
-    fun decomp_genreif da cgns (t, ctxt) bds =
+    fun decomp_reify da cgns (t, ctxt) bds =
       let
         val thy = Proof_Context.theory_of ctxt;
         val cert = cterm_of thy;
@@ -168,7 +170,7 @@
             in
               ((fts ~~ replicate (length fts) ctxt,
                  apfst (FWD (Drule.instantiate_normalize (ctyenv, its) cong))), bds)
-            end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
+            end handle Pattern.MATCH => decomp_reify da congs (t,ctxt) bds))
       end;
 
  (* looks for the atoms equation and instantiates it with the right number *)
@@ -268,7 +270,7 @@
 
     val (congs, bds) = mk_congs ctxt eqs;
     val congs = rearrange congs;
-    val (th, bds) = divide_and_conquer' (decomp_genreif (mk_decompatom eqs) congs) (t,ctxt) bds;
+    val (th, bds) = divide_and_conquer' (decomp_reify (mk_decompatom eqs) congs) (t,ctxt) bds;
     fun is_listVar (Var (_, t)) = can dest_listT t
       | is_listVar _ = false;
     val vars = th |> prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd
@@ -282,9 +284,9 @@
       (fn _ => simp_tac ctxt 1)
   in FWD trans [th'',th'] end;
 
-fun gen_reflect ctxt conv corr_thms eqs t =
+fun reflect ctxt conv corr_thms eqs t =
   let
-    val reify_thm = gen_reify ctxt eqs t;
+    val reify_thm = reify ctxt eqs t;
     fun try_corr thm =
       SOME (FWD trans [reify_thm, thm RS sym]) handle THM _ => NONE;
     val thm = case get_first try_corr corr_thms
@@ -304,11 +306,11 @@
     val thm = mk_thm t RS ssubst;
   in rtac thm i end);
  
-fun gen_reify_tac ctxt eqs = tac_of_thm (gen_reify ctxt eqs);
+fun reify_tac ctxt eqs = tac_of_thm (reify ctxt eqs);
 
 (*Reflection calls reification and uses the correctness theorem assumed to be the head of the list*)
-fun gen_reflection_tac ctxt conv corr_thms eqs =
-  tac_of_thm (gen_reflect ctxt conv corr_thms eqs);
+fun reflection_tac ctxt conv corr_thms eqs =
+  tac_of_thm (reflect ctxt conv corr_thms eqs);
 
 structure Data = Generic_Data
 (
@@ -340,7 +342,7 @@
     val { reification_eqs = default_eqs, correctness_thms = _ } =
       get_default ctxt;
     val eqs = fold Thm.add_thm user_eqs default_eqs;
-  in gen_reify_tac ctxt eqs end;
+  in reify_tac ctxt eqs end;
 
 fun default_reflection_tac ctxt user_thms user_eqs =
   let
@@ -350,7 +352,7 @@
     val eqs = fold Thm.add_thm user_eqs default_eqs; 
     val conv = Code_Evaluation.dynamic_conv (Proof_Context.theory_of ctxt);
       (*FIXME why Code_Evaluation.dynamic_conv? very specific*)
-  in gen_reflection_tac ctxt conv corr_thms eqs end;
+  in reflection_tac ctxt conv corr_thms eqs end;
 
 
 end