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