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/Nitpick_Examples/minipick.ML
changeset 59970 e9f73d87d904
parent 59058 a78612c67ec0
child 69597 ff784d5a5bfb 
--- a/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 16:24:22 2015 +0200
+++ b/src/HOL/Nitpick_Examples/minipick.ML	Wed Apr 08 19:39:08 2015 +0200
@@ -409,7 +409,7 @@
       | concrete (Type (@{type_name prod}, Ts)) = forall concrete Ts
       | concrete _ = true
     val neg_t =
-      @{const Not} $ Object_Logic.atomize_term thy t
+      @{const Not} $ Object_Logic.atomize_term ctxt t
       |> map_types unsetify_type
     val _ = fold_types (K o check_type ctxt raw_infinite) neg_t ()
     val frees = Term.add_frees neg_t []
isabelle