--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 15:14:38 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Jul 14 16:50:05 2011 +0200
@@ -1229,11 +1229,6 @@
| is_ground_term (Const _) = true
| is_ground_term _ = false
-fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
- | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
- | hashw_term _ = 0w0
-val hash_term = Word.toInt o hashw_term
-
fun special_bounds ts =
fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)