diff -r 8dbe623a7804 -r f732a674db1b src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 15 17:27:24 2013 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed May 15 17:43:42 2013 +0200
@@ -656,7 +656,7 @@
                          #> pairself (Envir.subst_term_types tyenv))
           val tysubst = tyenv |> Vartab.dest
         in (tysubst, tsubst) end
-      fun subst_info_for_prem subgoal_no prem =
+      fun subst_info_of_prem subgoal_no prem =
         case prem of
           _ $ (Const (@{const_name Meson.skolem}, _) $ (_ $ t $ num)) =>
           let val ax_no = HOLogic.dest_nat num in
@@ -675,7 +675,7 @@
             NONE
       fun clusters_in_term skolem t =
         Term.add_var_names t [] |> map_filter (cluster_of_var_name skolem o fst)
-      fun deps_for_term_subst (var, t) =
+      fun deps_of_term_subst (var, t) =
         case clusters_in_term false var of
           [] => NONE
         | [(ax_no, cluster_no)] =>
@@ -684,9 +684,9 @@
                 |> cluster_no > 1 ? cons (ax_no, cluster_no - 1))
         | _ => raise TERM ("discharge_skolem_premises: Expected Var", [var])
       val prems = Logic.strip_imp_prems (prop_of prems_imp_false)
-      val substs = prems |> map2 subst_info_for_prem (1 upto length prems)
+      val substs = prems |> map2 subst_info_of_prem (1 upto length prems)
                          |> sort (int_ord o pairself fst)
-      val depss = maps (map_filter deps_for_term_subst o snd o snd o snd) substs
+      val depss = maps (map_filter deps_of_term_subst o snd o snd o snd) substs
       val clusters = maps (op ::) depss
       val ordered_clusters =
         Int_Pair_Graph.empty
@@ -720,7 +720,7 @@
                          cluster_no = 0 andalso skolem)
            |> sort shuffle_ord |> map (fst o snd)
 (* for debugging only:
-      fun string_for_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
+      fun string_of_subst_info (ax_no, (subgoal_no, (tysubst, tsubst))) =
         "ax: " ^ string_of_int ax_no ^ "; asm: " ^ string_of_int subgoal_no ^
         "; tysubst: " ^ @{make_string} tysubst ^ "; tsubst: {" ^
         commas (map ((fn (s, t) => s ^ " |-> " ^ t)
@@ -729,12 +729,12 @@
       val _ = tracing ("AXIOM COUNTS: " ^ @{make_string} ax_counts)
       val _ = tracing ("OUTER PARAMS: " ^ @{make_string} outer_param_names)
       val _ = tracing ("SUBSTS (" ^ string_of_int (length substs) ^ "):\n" ^
-                       cat_lines (map string_for_subst_info substs))
+                       cat_lines (map string_of_subst_info substs))
 *)
       fun cut_and_ex_tac axiom =
         cut_tac axiom 1
         THEN TRY (REPEAT_ALL_NEW (etac @{thm exE}) 1)
-      fun rotation_for_subgoal i =
+      fun rotation_of_subgoal i =
         find_index (fn (_, (subgoal_no, _)) => subgoal_no = i) substs
     in
       Goal.prove ctxt [] [] @{prop False}
@@ -746,7 +746,7 @@
               THEN match_tac [prems_imp_false] 1
               THEN ALLGOALS (fn i =>
                        rtac @{thm Meson.skolem_COMBK_I} i
-                       THEN rotate_tac (rotation_for_subgoal i) i
+                       THEN rotate_tac (rotation_of_subgoal i) i
                        THEN PRIMITIVE (unify_first_prem_with_concl thy i)
                        THEN assume_tac i
                        THEN flexflex_tac)))