# HG changeset patch
# User krauss
# Date 1192722270 -7200
# Node ID 9a13ab12b174b75ef990119ca2ac4120925c7bcc
# Parent  5908591fb881aa40fb40aa600b0c74e9051bc79e
Simultaneous type inference using read_specification

diff -r 5908591fb881 -r 9a13ab12b174 src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 18 17:38:45 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Oct 18 17:44:30 2007 +0200
@@ -88,22 +88,9 @@
     end (* FIXME: Add cases for induct and cases thm *)
 
 
-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')))
-
-      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 *)
-    in
-      ((fixes, spec), ctxt')
-    end
-
 fun gen_add_fundef prep fixspec eqnss config flags lthy =
     let
-      val ((fixes, spec), ctxt') = prepare_spec prep fixspec eqnss lthy
+      val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
       val (eqs, post, sort_cont) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
 
       val defname = mk_defname fixes