src/HOL/Tools/function_package/fundef_package.ML
changeset 24722 59fd5cceccd7
parent 24711 e8bba7723858
child 24830 a7b3ab44d993
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 26 19:17:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Wed Sep 26 19:17:57 2007 +0200
     1.3 @@ -88,12 +88,12 @@
     1.4      end (* FIXME: Add cases for induct and cases thm *)
     1.5  
     1.6  
     1.7 -fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete when "read_specification" etc. is there *)
     1.8 +fun prepare_spec prep fixspec eqnss lthy = (* FIXME: obsolete; use Specification.read/check_specification *)
     1.9      let
    1.10        val eqns = map (apsnd single) eqnss
    1.11  
    1.12        val ((fixes, _), ctxt') = prep fixspec [] lthy             
    1.13 -      fun prep_eqn e = the_single (snd (fst (prep [] [e] ctxt')))
    1.14 +      fun prep_eqn e = the_single (snd (fst (prep [] [[e]] ctxt')))
    1.15  
    1.16        val spec = map prep_eqn eqns
    1.17                   |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
    1.18 @@ -162,7 +162,7 @@
    1.19  
    1.20  
    1.21  val add_fundef = gen_add_fundef Specification.read_specification
    1.22 -val add_fundef_i = gen_add_fundef Specification.cert_specification
    1.23 +val add_fundef_i = gen_add_fundef Specification.check_specification
    1.24  
    1.25  
    1.26  (* Datatype hook to declare datatype congs as "fundef_congs" *)