--- a/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 12 21:47:36 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Thu Mar 12 21:51:02 2009 +0100
@@ -93,13 +93,12 @@
end
-fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqns config flags lthy =
let
val constrn_fxs = map (fn (b, T, mx) => (b, SOME (the_default default_constraint T), mx))
- val ((fixes0, spec0), ctxt') =
- prep (constrn_fxs fixspec) (map (single o apsnd single) eqnss) lthy
+ val ((fixes0, spec0), ctxt') = prep (constrn_fxs fixspec) eqns lthy
val fixes = map (apfst (apfst Binding.name_of)) fixes0;
- val spec = map (apfst (apfst Binding.name_of)) spec0;
+ val spec = map (fn ((b, atts), prop) => ((Binding.name_of b, atts), [prop])) spec0;
val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
val defname = mk_defname fixes
@@ -163,9 +162,8 @@
|> LocalTheory.set_group (serial_string ())
|> setup_termination_proof term_opt;
-val add_fundef = gen_add_fundef true Specification.read_specification "_::type"
-val add_fundef_i =
- gen_add_fundef false Specification.check_specification (TypeInfer.anyT HOLogic.typeS)
+val add_fundef = gen_add_fundef true Specification.read_spec "_::type"
+val add_fundef_i = gen_add_fundef false Specification.check_spec (TypeInfer.anyT HOLogic.typeS)
(* Datatype hook to declare datatype congs as "fundef_congs" *)