src/HOL/Tools/choice_specification.ML

 Package for defining constants by specification.
 *)
 
 signature CHOICE_SPECIFICATION =
 sig
+  val close_form : term -> term
   val add_specification: string option -> (bstring * xstring * bool) list ->
     theory * thm -> theory * thm
 end
 
 structure Choice_Specification: CHOICE_SPECIFICATION =
 struct
 
 (* actual code *)
+
+fun close_form t =
+    fold_rev (fn (s, T) => fn t => HOLogic.mk_all (s, T, t))
+             (map dest_Free (OldTerm.term_frees t)) t
 
 local
     fun mk_definitional [] arg = arg
       | mk_definitional ((thname,cname,covld)::cos) (thy,thm) =
         case HOLogic.dest_Trueprop (concl_of thm) of

         fun proc_single prop =
             let
                 val frees = OldTerm.term_frees prop
                 val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
                   orelse error "Specificaton: Only free variables of sort 'type' allowed"
-                val prop_closed = fold_rev (fn (vname, T) => fn prop =>
-                  HOLogic.mk_all (vname, T, prop)) (map dest_Free frees) prop
+                val prop_closed = close_form prop
             in
                 (prop_closed,frees)
             end
 
         val props'' = map proc_single props'

                                   PureThy.store_thm (Binding.name name, thm) thy)
                     in
                         args |> apsnd (remove_alls frees)
                              |> apsnd undo_imps
                              |> apsnd Drule.export_without_context
-                             |> Thm.theory_attributes (map (Attrib.attribute thy) atts)
+                             |> Thm.theory_attributes (map (Attrib.attribute thy)
+                                                           (Attrib.internal (K Nitpick_Choice_Specs.add) :: atts))
                              |> add_final
                              |> Library.swap
                     end
 
                 fun process_all [proc_arg] args =