Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 56243 2e10a36b8d46
parent 56220 4c43a2881b25
child 56245 84fc7dfa3cd4 
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 21 12:34:50 2014 +0100
@@ -1444,7 +1444,7 @@
 fun normalized_rhs_of t =
   let
     fun aux (v as Var _) (SOME t) = SOME (lambda v t)
-      | aux (c as Const (@{const_name TYPE}, _)) (SOME t) = SOME (lambda c t)
+      | aux (c as Const (@{const_name Pure.type}, _)) (SOME t) = SOME (lambda c t)
       | aux _ _ = NONE
     val (lhs, rhs) =
       case t of
isabelle