specification goal: eliminated redundant Thm.legacy_freezeT -- the goal is properly declared and should always produce fixed types in the result;
specification result: replaced Thm.legacy_freezeT by Thm.unvarify_global -- the final result appears to be a closed term that is globally exported;

--- a/src/HOL/Tools/choice_specification.ML	Mon May 03 22:00:06 2010 +0200
+++ b/src/HOL/Tools/choice_specification.ML	Tue May 04 10:52:43 2010 +0200
@@ -78,10 +78,9 @@
       | NONE => mk_definitional cos arg
 end
 
-fun add_specification axiomatic cos arg =
-    arg |> apsnd Thm.legacy_freezeT
-        |> proc_exprop axiomatic cos
-        |> apsnd Drule.export_without_context
+fun add_specification axiomatic cos =
+    proc_exprop axiomatic cos
+    #> apsnd Drule.export_without_context
 
 
 (* Collect all intances of constants in term *)
@@ -217,15 +216,16 @@
                         then writeln "specification"
                         else ()
             in
-                arg |> apsnd Thm.legacy_freezeT
+                arg |> apsnd Thm.unvarify_global
                     |> process_all (zip3 alt_names rew_imps frees)
             end
 
-      fun after_qed [[thm]] = ProofContext.theory (fn thy =>
-        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm))));
+      fun after_qed [[thm]] = (ProofContext.theory (fn thy =>
+        #1 (post_process (add_specification axiomatic (zip3 names cnames overloaded) (thy, thm)))));
     in
       thy
       |> ProofContext.init_global
+      |> Variable.declare_term ex_prop
       |> Proof.theorem NONE after_qed [[(HOLogic.mk_Trueprop ex_prop, [])]]
     end;