# HG changeset patch
# User krauss
# Date 1228982542 -3600
# Node ID b9c5726e79ab66744a854c8335ef10399e9419c2
# Parent  cc9a25916582bfe362026120d8c4607c0f657db0
constrain type inference to sort "type"

diff -r cc9a25916582 -r b9c5726e79ab src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Wed Dec 10 17:22:34 2008 -0800
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Thu Dec 11 09:02:22 2008 +0100
@@ -93,9 +93,11 @@
     end
 
 
-fun gen_add_fundef is_external prep fixspec eqnss config flags lthy =
+fun gen_add_fundef is_external prep default_constraint fixspec eqnss config flags lthy =
     let
-      val ((fixes0, spec0), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
+      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 fixes = map (apfst (apfst Binding.base_name)) fixes0;
       val spec = map (apfst (apfst Binding.base_name)) spec0;
       val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
@@ -160,8 +162,9 @@
   |> LocalTheory.set_group (serial_string ())
   |> setup_termination_proof term_opt;
 
-val add_fundef = gen_add_fundef true Specification.read_specification
-val add_fundef_i = gen_add_fundef false Specification.check_specification
+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)
 
 
 (* Datatype hook to declare datatype congs as "fundef_congs" *)