src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 43827 62d64709af3b
parent 43085 0a2f5b86bdd7
child 44012 8c1dfd6c2262
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 15:14:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Jul 14 16:50:05 2011 +0200
     1.3 @@ -1229,11 +1229,6 @@
     1.4    | is_ground_term (Const _) = true
     1.5    | is_ground_term _ = false
     1.6  
     1.7 -fun hashw_term (t1 $ t2) = hashw (hashw_term t1, hashw_term t2)
     1.8 -  | hashw_term (Const (s, _)) = hashw_string (s, 0w0)
     1.9 -  | hashw_term _ = 0w0
    1.10 -val hash_term = Word.toInt o hashw_term
    1.11 -
    1.12  fun special_bounds ts =
    1.13    fold Term.add_vars ts [] |> sort (Term_Ord.fast_indexname_ord o pairself fst)
    1.14