src/HOL/Tools/specification_package.ML

         SOME axname => mk_axiomatic axname cos (apsnd (HOLogic.dest_Trueprop o concl_of) arg)
       | NONE => mk_definitional cos arg
 end
 
 fun add_specification axiomatic cos arg =
-    arg |> apsnd freezeT
+    arg |> apsnd Thm.freezeT
         |> proc_exprop axiomatic cos
         |> apsnd standard
 
 fun add_spec x y (context, thm) =
   (Context.the_theory context, thm) |> add_specification x y |>> Context.Theory;

                 val alt_names = map fst alt_props
                 val _ = if exists (fn(name,_) => not (name = "")) alt_names
                         then writeln "specification"
                         else ()
             in
-                arg |> apsnd freezeT
+                arg |> apsnd Thm.freezeT
                     |> process_all (zip3 alt_names rew_imps frees)
             end
             fun post_proc (context, th) =
                 post_process (Context.theory_of context, th) |>> Context.Theory;
     in