# HG changeset patch
# User wenzelm
# Date 1190827077 -7200
# Node ID 59fd5cceccd7bd9b05b06b54ad1d8d1be7438654
# Parent  2a029b78db60c20ed7965682a502925c6cb91ec7
minimal adaptions for Specification.read/check_specification;

diff -r 2a029b78db60 -r 59fd5cceccd7 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 26 19:17:56 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 26 19:17:57 2007 +0200
@@ -88,12 +88,12 @@
     end (* FIXME: Add cases for induct and cases thm *)
 
 
-fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *)
+fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete; use Specification.read/check_specification *)
     let
       val eqns = map (apsnd single) eqnss
 
       val ((fixes, _), ctxt') = prep fixspec [] lthy             
-      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
+      fun prep_eqn e = the_single (snd (fst (prep [] [[e]] ctxt')))
 
       val spec = map prep_eqn eqns
                  |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
@@ -162,7 +162,7 @@
 
 
 val add_fundef = gen_add_fundef Specification.read_specification
-val add_fundef_i = gen_add_fundef Specification.cert_specification
+val add_fundef_i = gen_add_fundef Specification.check_specification
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)