Simultaneous type inference using read_specification
authorkrauss
Thu Oct 18 17:44:30 2007 +0200 (2007-10-18)
changeset 250889a13ab12b174
parent 25087 5908591fb881
child 25089 04b8456f7754
Simultaneous type inference using read_specification
src/HOL/Tools/function_package/fundef_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 18 17:38:45 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 18 17:44:30 2007 +0200
     1.3 @@ -88,22 +88,9 @@
     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; use Specification.read/check_specification *)
     1.8 -    let
     1.9 -      val eqns = map (apsnd single) eqnss
    1.10 -
    1.11 -      val ((fixes, _), ctxt') = prep fixspec [] lthy             
    1.12 -      fun prep_eqn e = the_single (snd (fst (prep [] [[e]] ctxt')))
    1.13 -
    1.14 -      val spec = map prep_eqn eqns
    1.15 -                 |> map (apsnd (map (fn t => fold_rev (mk_forall o Free) (frees_in_term ctxt' t) t))) (* Add quantifiers *)
    1.16 -    in
    1.17 -      ((fixes, spec), ctxt')
    1.18 -    end
    1.19 -
    1.20  fun gen_add_fundef prep fixspec eqnss config flags lthy =
    1.21      let
    1.22 -      val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
    1.23 +      val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
    1.24        val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.25  
    1.26        val defname = mk_defname fixes