# HG changeset patch
# User blanchet
# Date 1354574633 -3600
# Node ID 73f2f0cd4aea9f89d7bd13c290dae19159738e4b
# Parent  68555697f37e57b4ffac2c97c9638dbdc92bffe2
tuned names

diff -r 68555697f37e -r 73f2f0cd4aea src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 03 23:43:52 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 03 23:43:53 2012 +0100
@@ -491,18 +491,18 @@
     fun mk_app s args =
       if member (op <>) args "" then s ^ "(" ^ space_implode "," args ^ ")"
       else s
-    fun patternify ~1 _ = ""
-      | patternify depth t =
+    fun patternify_term ~1 _ = ""
+      | patternify_term depth t =
         case strip_comb t of
           (Const (x as (s, _)), args) =>
           if is_bad_const x args then ""
-          else mk_app (const_name_of s) (map (patternify (depth - 1)) args)
+          else mk_app (const_name_of s) (map (patternify_term (depth - 1)) args)
         | _ => ""
-    fun add_pattern depth t =
-      case patternify depth t of "" => I | s => insert (op =) s
+    fun add_term_pattern depth t =
+      case patternify_term depth t of "" => I | s => insert (op =) s
     fun add_term_patterns ~1 _ = I
       | add_term_patterns depth t =
-        add_pattern depth t #> add_term_patterns (depth - 1) t
+        add_term_pattern depth t #> add_term_patterns (depth - 1) t
     val add_term = add_term_patterns term_max_depth
     fun add_patterns t =
       let val (head, args) = strip_comb t in