# HG changeset patch
# User blanchet
# Date 1362748539 -3600
# Node ID cac8c9a636b6334cda739d651260624eb13a5373
# Parent  6dd83e007f56fc3fffa74433d72a62a22cc8fa1e
proper type inference for default values

diff -r 6dd83e007f56 -r cac8c9a636b6 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Mar 08 13:21:58 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Fri Mar 08 14:15:39 2013 +0100
@@ -1165,7 +1165,7 @@
 
 val datatypes = define_datatypes (K I) (K I) (K I);
 
-val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.read_term;
+val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
diff -r 6dd83e007f56 -r cac8c9a636b6 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Mar 08 13:21:58 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Fri Mar 08 14:15:39 2013 +0100
@@ -167,7 +167,6 @@
              SOME disc)) ks ms ctrs0;
 
     val no_discs = map is_none disc_bindings;
-    val no_discs_at_all = forall I no_discs;
 
     fun std_sel_binding m l = Binding.name o mk_unN m l o base_name_of_ctr;
 
@@ -240,19 +239,13 @@
           fun alternate_disc k =
             Term.lambda u (alternate_disc_lhs (K o rapp u o disc_free) (3 - k));
 
-          fun mk_default T t =
-            let
-              val Ts0 = map TFree (Term.add_tfreesT (fastype_of t) []);
-              val Ts = map TFree (Term.add_tfreesT T []);
-            in Term.subst_atomic_types (Ts0 ~~ Ts) t end;
-
           fun mk_sel_case_args b proto_sels T =
             map2 (fn Ts => fn k =>
               (case AList.lookup (op =) proto_sels k of
                 NONE =>
                 (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
                   NONE => fold_rev (Term.lambda o curry Free Name.uu) Ts (mk_undefined T)
-                | SOME t => mk_default (Ts ---> T) t)
+                | SOME t => t |> Type.constraint (Ts ---> T) |> Syntax.check_term no_defs_lthy)
               | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
 
           fun sel_spec b proto_sels =
@@ -658,7 +651,7 @@
 
 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_wrap_datatype Syntax.read_term;
+  prepare_wrap_datatype Syntax.parse_term;
 
 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};