src/HOL/Tools/specification_package.ML

--- a/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:11 2008 +0100
+++ b/src/HOL/Tools/specification_package.ML	Wed Dec 31 00:08:13 2008 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/specification_package.ML
-    ID:         $Id$
     Author:     Sebastian Skalberg, TU Muenchen
 
 Package for defining constants by specification.
@@ -118,7 +117,7 @@
 
         fun proc_single prop =
             let
-                val frees = Term.term_frees prop
+                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 = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) prop (map dest_Free frees)