# HG changeset patch # User nipkow # Date 1247028210 -7200 # Node ID 683b5e3b31fc0591f85c772da6b0cd8c3e688d7a # Parent 3fc19d2f0ac9e3d731c0cee149ba8d08997fd9c5# Parent 1984af09eb41aba545f74ed628739a021964e86b merged diff -r 1984af09eb41 -r 683b5e3b31fc src/HOL/Extraction/Euclid.thy --- a/src/HOL/Extraction/Euclid.thy Wed Jul 08 06:42:35 2009 +0200 +++ b/src/HOL/Extraction/Euclid.thy Wed Jul 08 06:43:30 2009 +0200 @@ -189,7 +189,7 @@ assume pn: "p \ n" from `prime p` have "0 < p" by (rule prime_g_zero) then have "p dvd n!" using pn by (rule dvd_factorial) - with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff) + with dvd have "p dvd ?k - n!" by (rule dvd_diff_nat) then have "p dvd 1" by simp with prime show False using prime_nd_one by auto qed diff -r 1984af09eb41 -r 683b5e3b31fc src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Jul 08 06:42:35 2009 +0200 +++ b/src/HOL/HOL.thy Wed Jul 08 06:43:30 2009 +0200 @@ -1869,7 +1869,27 @@ declare simp_thms(6) [code nbe] setup {* - Code.add_const_alias @{thm equals_eq} + Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\type \ 'a \ bool"}) +*} + +lemma equals_alias_cert: "OFCLASS('a, eq_class) \ ((op = :: 'a \ 'a \ bool) \ eq)" (is "?ofclass \ ?eq") +proof + assume "PROP ?ofclass" + show "PROP ?eq" + by (tactic {* ALLGOALS (rtac (Drule.unconstrainTs @{thm equals_eq})) *}) + (fact `PROP ?ofclass`) +next + assume "PROP ?eq" + show "PROP ?ofclass" proof + qed (simp add: `PROP ?eq`) +qed + +setup {* + Sign.add_const_constraint (@{const_name eq}, SOME @{typ "'a\eq \ 'a \ bool"}) +*} + +setup {* + Code.add_const_alias @{thm equals_alias_cert} *} hide (open) const eq diff -r 1984af09eb41 -r 683b5e3b31fc src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Wed Jul 08 06:42:35 2009 +0200 +++ b/src/HOL/Library/Efficient_Nat.thy Wed Jul 08 06:43:30 2009 +0200 @@ -105,15 +105,9 @@ This can be accomplished by applying the following transformation rules: *} -lemma Suc_if_eq': "(\n. f (Suc n) = h n) \ f 0 = g \ - f n = (if n = 0 then g else h (n - 1))" - by (cases n) simp_all - lemma Suc_if_eq: "(\n. f (Suc n) \ h n) \ f 0 \ g \ f n \ if n = 0 then g else h (n - 1)" - by (rule eq_reflection, rule Suc_if_eq') - (rule meta_eq_to_obj_eq, assumption, - rule meta_eq_to_obj_eq, assumption) + by (rule eq_reflection) (cases n, simp_all) lemma Suc_clause: "(\n. P n (Suc n)) \ n \ 0 \ P (n - 1) n" by (cases n) simp_all @@ -129,14 +123,14 @@ setup {* let -fun gen_remove_suc Suc_if_eq dest_judgement thy thms = +fun remove_suc thy thms = let val vname = Name.variant (map fst (fold (Term.add_var_names o Thm.full_prop_of) thms [])) "n"; val cv = cterm_of thy (Var ((vname, 0), HOLogic.natT)); fun lhs_of th = snd (Thm.dest_comb - (fst (Thm.dest_comb (dest_judgement (cprop_of th))))); - fun rhs_of th = snd (Thm.dest_comb (dest_judgement (cprop_of th))); + (fst (Thm.dest_comb (cprop_of th)))); + fun rhs_of th = snd (Thm.dest_comb (cprop_of th)); fun find_vars ct = (case term_of ct of (Const (@{const_name Suc}, _) $ Var _) => [(cv, snd (Thm.dest_comb ct))] | _ $ _ => @@ -156,7 +150,7 @@ (Drule.instantiate' [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct), SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv'] - Suc_if_eq)) (Thm.forall_intr cv' th) + @{thm Suc_if_eq})) (Thm.forall_intr cv' th) in case map_filter (fn th'' => SOME (th'', singleton @@ -169,21 +163,19 @@ end in get_first mk_thms eqs end; -fun gen_eqn_suc_preproc Suc_if_eq dest_judgement dest_lhs thy thms = +fun eqn_suc_preproc thy thms = let - val dest = dest_lhs o prop_of; + val dest = fst o Logic.dest_equals o prop_of; val contains_suc = exists_Const (fn (c, _) => c = @{const_name Suc}); in if forall (can dest) thms andalso exists (contains_suc o dest) thms - then perhaps_loop (gen_remove_suc Suc_if_eq dest_judgement thy) thms + then perhaps_loop (remove_suc thy) thms else NONE end; -val eqn_suc_preproc = Code_Preproc.simple_functrans (gen_eqn_suc_preproc - @{thm Suc_if_eq} I (fst o Logic.dest_equals)); +val eqn_suc_preproc1 = Code_Preproc.simple_functrans eqn_suc_preproc; -fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc - @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms +fun eqn_suc_preproc2 thy thms = eqn_suc_preproc thy thms |> the_default thms; fun remove_suc_clause thy thms = @@ -227,9 +219,9 @@ end; in - Codegen.add_preprocessor eqn_suc_preproc' + Codegen.add_preprocessor eqn_suc_preproc2 #> Codegen.add_preprocessor clause_suc_preproc - #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc) + #> Code_Preproc.add_functrans ("eqn_Suc", eqn_suc_preproc1) end; *} diff -r 1984af09eb41 -r 683b5e3b31fc src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/HOL/Tools/recfun_codegen.ML Wed Jul 08 06:43:30 2009 +0200 @@ -29,22 +29,14 @@ val (thm', _) = Code.mk_eqn thy (K false) (thm, true) in thy - |> ModuleData.map (Symtab.update (Code.const_eqn thy thm', module_name)) + |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name)) |> Code.add_eqn thm' end; -fun meta_eq_to_obj_eq thy thm = - let - val T = (fastype_of o fst o Logic.dest_equals o Thm.prop_of) thm; - in if Sign.of_sort thy (T, @{sort type}) - then SOME (Conv.fconv_rule Drule.beta_eta_conversion (@{thm meta_eq_to_obj_eq} OF [thm])) - else NONE - end; - fun expand_eta thy [] = [] | expand_eta thy (thms as thm :: _) = let - val (_, ty) = Code.const_typ_eqn thm; + val (_, ty) = Code.const_typ_eqn thy thm; in if null (Term.add_tvarsT ty []) orelse (null o fst o strip_type) ty then thms else map (Code.expand_eta thy 1) thms @@ -57,12 +49,11 @@ val thms = Code.these_eqns thy c' |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |> expand_eta thy - |> map_filter (meta_eq_to_obj_eq thy) |> Code.norm_varnames thy |> map (rpair opt_name) in if null thms then NONE else SOME thms end; -val dest_eqn = HOLogic.dest_eq o HOLogic.dest_Trueprop; +val dest_eqn = Logic.dest_equals; val const_of = dest_Const o head_of o fst o dest_eqn; fun get_equations thy defs (s, T) = diff -r 1984af09eb41 -r 683b5e3b31fc src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/Pure/Isar/code.ML Wed Jul 08 06:43:30 2009 +0200 @@ -7,22 +7,18 @@ signature CODE = sig + (*constants*) + val string_of_const: theory -> string -> string + val args_number: theory -> string -> int + val check_const: theory -> term -> string + val read_bare_const: theory -> string -> string * typ + val read_const: theory -> string -> string + val typscheme: theory -> string * typ -> (string * sort) list * typ + (*constructor sets*) val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * typ list) list) - (*typ instantiations*) - val typscheme: theory -> string * typ -> (string * sort) list * typ - val inst_thm: theory -> sort Vartab.table -> thm -> thm - - (*constants*) - val string_of_typ: theory -> typ -> string - val string_of_const: theory -> string -> string - val no_args: theory -> string -> int - val check_const: theory -> term -> string - val read_bare_const: theory -> string -> string * typ - val read_const: theory -> string -> string - (*constant aliasses*) val add_const_alias: thm -> theory -> theory val triv_classes: theory -> class list @@ -35,22 +31,12 @@ val assert_eqn: theory -> thm * bool -> thm * bool val assert_eqns_const: theory -> string -> (thm * bool) list -> (thm * bool) list - val const_typ_eqn: thm -> string * typ - val const_eqn: theory -> thm -> string + val const_typ_eqn: theory -> thm -> string * typ val typscheme_eqn: theory -> thm -> (string * sort) list * typ val expand_eta: theory -> int -> thm -> thm - val rewrite_eqn: simpset -> thm -> thm - val rewrite_head: thm list -> thm -> thm val norm_args: theory -> thm list -> thm list val norm_varnames: theory -> thm list -> thm list - (*case certificates*) - val case_cert: thm -> string * (int * string list) - - (*infrastructure*) - val add_attribute: string * attribute parser -> theory -> theory - val purge_data: theory -> theory - (*executable content*) val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory @@ -58,25 +44,26 @@ (string * ((string * sort) list * (string * typ list) list) -> theory -> theory) -> theory -> theory val add_eqn: thm -> theory -> theory + val add_eqnl: string * (thm * bool) list lazy -> theory -> theory val add_nbe_eqn: thm -> theory -> theory val add_default_eqn: thm -> theory -> theory val add_default_eqn_attribute: attribute val add_default_eqn_attrib: Attrib.src val del_eqn: thm -> theory -> theory val del_eqns: string -> theory -> theory - val add_eqnl: string * (thm * bool) list lazy -> theory -> theory val add_case: thm -> theory -> theory val add_undefined: string -> theory -> theory - - (*data retrieval*) val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option - val default_typscheme: theory -> string -> (string * sort) list * typ val these_eqns: theory -> string -> (thm * bool) list val all_eqns: theory -> (thm * bool) list val get_case_scheme: theory -> string -> (int * (int * string list)) option val undefineds: theory -> string list val print_codesetup: theory -> unit + + (*infrastructure*) + val add_attribute: string * attribute parser -> theory -> theory + val purge_data: theory -> theory end; signature CODE_DATA_ARGS = @@ -117,7 +104,7 @@ of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) | NONE => Sign.extern_const thy c; -fun no_args thy = length o fst o strip_type o Sign.the_const_type thy; +fun args_number thy = length o fst o strip_type o Sign.the_const_type thy; (* utilities *) @@ -125,21 +112,7 @@ fun typscheme thy (c, ty) = let val ty' = Logic.unvarifyT ty; - fun dest (TFree (v, sort)) = (v, sort) - | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); - val vs = map dest (Sign.const_typargs thy (c, ty')); - in (vs, Type.strip_sorts ty') end; - -fun inst_thm thy tvars' thm = - let - val tvars = (Term.add_tvars o Thm.prop_of) thm []; - val inter_sort = Sorts.inter_sort (Sign.classes_of thy); - fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v - of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) - (tvar, (v, inter_sort (sort, sort')))) - | NONE => NONE; - val insts = map_filter mk_inst tvars; - in Thm.instantiate (insts, []) thm end; + in (map dest_TFree (Sign.const_typargs thy (c, ty')), Type.strip_sorts ty') end; fun expand_eta thy k thm = let @@ -173,23 +146,6 @@ |> Conv.fconv_rule Drule.beta_eta_conversion end; -fun eqn_conv conv = - let - fun lhs_conv ct = if can Thm.dest_comb ct - then (Conv.combination_conv lhs_conv conv) ct - else Conv.all_conv ct; - in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; - -fun head_conv conv = - let - fun lhs_conv ct = if can Thm.dest_comb ct - then (Conv.fun_conv lhs_conv) ct - else conv ct; - in Conv.fun_conv (Conv.arg_conv lhs_conv) end; - -val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; -val rewrite_head = Conv.fconv_rule o head_conv o MetaSimplifier.rewrite false; - fun norm_args thy thms = let val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals; @@ -265,6 +221,19 @@ end; +(* reading constants as terms *) + +fun check_bare_const thy t = case try dest_Const t + of SOME c_ty => c_ty + | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); + +fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; + +fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; + +fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; + + (* const aliasses *) structure ConstAlias = TheoryDataFun @@ -280,16 +249,29 @@ fun add_const_alias thm thy = let - val lhs_rhs = case try Logic.dest_equals (Thm.prop_of thm) + val (ofclass, eqn) = case try Logic.dest_equals (Thm.prop_of thm) + of SOME ofclass_eq => ofclass_eq + | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); + val (T, class) = case try Logic.dest_of_class ofclass + of SOME T_class => T_class + | _ => error ("Bad certificate: " ^ Display.string_of_thm thm); + val tvar = case try Term.dest_TVar T + of SOME tvar => tvar + | _ => error ("Bad type: " ^ Display.string_of_thm thm); + val _ = if Term.add_tvars eqn [] = [tvar] then () + else error ("Inconsistent type: " ^ Display.string_of_thm thm); + val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs - | _ => error ("Not an equation: " ^ Display.string_of_thm thm); - val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs + | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); + val c_c' = case try (pairself (check_const thy)) lhs_rhs of SOME c_c' => c_c' - | _ => error ("Not an equation with two constants: " ^ Display.string_of_thm thm); - val some_class = the_list (AxClass.class_of_param thy (snd c_c')); + | _ => error ("Not an equation with two constants: " + ^ Syntax.string_of_term_global thy eqn); + val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then () + else error ("Inconsistent class: " ^ Display.string_of_thm thm); in thy |> ConstAlias.map (fn (alias, classes) => - ((c_c', thm) :: alias, fold (insert (op =)) some_class classes)) + ((c_c', thm) :: alias, insert (op =) class classes)) end; fun resubst_alias thy = @@ -306,19 +288,6 @@ val triv_classes = snd o ConstAlias.get; -(* reading constants as terms *) - -fun check_bare_const thy t = case try dest_Const t - of SOME c_ty => c_ty - | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t); - -fun check_const thy = AxClass.unoverload_const thy o check_bare_const thy; - -fun read_bare_const thy = check_bare_const thy o Syntax.read_term_global thy; - -fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy; - - (* constructor sets *) fun constrset_of_consts thy cs = @@ -440,8 +409,6 @@ fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); -val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; - (*those following are permissive wrt. to overloaded constants!*) @@ -456,14 +423,14 @@ o try_thm (gen_assert_eqn thy is_constr_head (K true)) o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); -fun const_typ_eqn_unoverload thy thm = +fun const_typ_eqn thy thm = let - val (c, ty) = const_typ_eqn thm; + val (c, ty) = (dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; val c' = AxClass.unoverload_const thy (c, ty); in (c', ty) end; -fun typscheme_eqn thy = typscheme thy o const_typ_eqn_unoverload thy; -fun const_eqn thy = fst o const_typ_eqn_unoverload thy; +fun typscheme_eqn thy = typscheme thy o const_typ_eqn thy; +fun const_eqn thy = fst o const_typ_eqn thy; (* case cerificates *) @@ -787,7 +754,7 @@ val dtyps = the_dtyps exec |> Symtab.dest |> map (fn (dtco, (_, (vs, cos)) :: _) => - (Syntax.string_of_typ_global thy (Type (dtco, map TFree vs)), cos)) + (string_of_typ thy (Type (dtco, map TFree vs)), cos)) |> sort (string_ord o pairself fst) in (Pretty.writeln o Pretty.chunks) [ @@ -817,7 +784,7 @@ val max' = Thm.maxidx_of thm' + 1; in (thm', max') end; val (thms', maxidx) = fold_map incr_thm thms 0; - val ty1 :: tys = map (snd o const_typ_eqn) thms'; + val ty1 :: tys = map (snd o const_typ_eqn thy) thms'; fun unify ty env = Sign.typ_unify thy (ty1, ty) env handle Type.TUNIFY => error ("Type unificaton failed, while unifying code equations\n" @@ -963,19 +930,6 @@ Symtab.dest ((the_eqns o the_exec) thy) |> maps (Lazy.force o snd o snd o fst o snd); -fun default_typscheme thy c = - let - fun the_const_typscheme c = (curry (typscheme thy) c o snd o dest_Const - o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c; - fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty); - in case AxClass.class_of_param thy c - of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c)) - | NONE => if is_constr thy c - then strip_sorts (the_const_typscheme c) - else case get_eqns thy c - of (thm, _) :: _ => (typscheme_eqn thy o Drule.zero_var_indexes) thm - | [] => strip_sorts (the_const_typscheme c) end; - end; (*struct*) diff -r 1984af09eb41 -r 683b5e3b31fc src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/Tools/Code/code_preproc.ML Wed Jul 08 06:43:30 2009 +0200 @@ -102,6 +102,15 @@ fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); +fun eqn_conv conv = + let + fun lhs_conv ct = if can Thm.dest_comb ct + then Conv.combination_conv lhs_conv conv ct + else Conv.all_conv ct; + in Conv.combination_conv (Conv.arg_conv lhs_conv) conv end; + +val rewrite_eqn = Conv.fconv_rule o eqn_conv o Simplifier.rewrite; + fun term_of_conv thy f = Thm.cterm_of thy #> f @@ -117,7 +126,7 @@ in eqns |> apply_functrans thy c functrans - |> (map o apfst) (Code.rewrite_eqn pre) + |> (map o apfst) (rewrite_eqn pre) |> (map o apfst) (AxClass.unoverload thy) |> map (Code.assert_eqn thy) |> burrow_fst (Code.norm_args thy) @@ -213,9 +222,19 @@ (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, Logic.unvarifyT ty)) | _ => I) (map (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Thm.plain_prop_of o fst) eqns); +fun default_typscheme_of thy c = + let + val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c + o Type.strip_sorts o Sign.the_const_type thy) c; + in case AxClass.class_of_param thy c + of SOME class => ([(Name.aT, [class])], ty) + | NONE => Code.typscheme thy (c, ty) + end; + fun tyscm_rhss_of thy c eqns = let - val tyscm = case eqns of [] => Code.default_typscheme thy c + val tyscm = case eqns + of [] => default_typscheme_of thy c | ((thm, _) :: _) => Code.typscheme_eqn thy thm; val rhss = consts_of thy eqns; in (tyscm, rhss) end; @@ -381,6 +400,17 @@ handle Sorts.CLASS_ERROR _ => [] (*permissive!*)) end; +fun inst_thm thy tvars' thm = + let + val tvars = (Term.add_tvars o Thm.prop_of) thm []; + val inter_sort = Sorts.inter_sort (Sign.classes_of thy); + fun mk_inst (tvar as (v, sort)) = case Vartab.lookup tvars' v + of SOME sort' => SOME (pairself (Thm.ctyp_of thy o TVar) + (tvar, (v, inter_sort (sort, sort')))) + | NONE => NONE; + val insts = map_filter mk_inst tvars; + in Thm.instantiate (insts, []) thm end; + fun add_arity thy vardeps (class, tyco) = AList.default (op =) ((class, tyco), map (fn k => (snd o Vargraph.get_node vardeps) (Inst (class, tyco), k)) @@ -394,7 +424,7 @@ val inst_tab = Vartab.empty |> fold (fn (v, sort) => Vartab.update ((v, 0), sort)) lhs; val eqns = proto_eqns - |> (map o apfst) (Code.inst_thm thy inst_tab); + |> (map o apfst) (inst_thm thy inst_tab); val (tyscm, rhss') = tyscm_rhss_of thy c eqns; val eqngr' = Graph.new_node (c, (tyscm, eqns)) eqngr; in (map (pair c) rhss' @ rhss, eqngr') end; diff -r 1984af09eb41 -r 683b5e3b31fc src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/Tools/Code/code_target.ML Wed Jul 08 06:43:30 2009 +0200 @@ -286,7 +286,7 @@ fun gen_add_syntax_const prep_const target raw_c raw_syn thy = let val c = prep_const thy raw_c; - fun check_args (syntax as (n, _)) = if n > Code.no_args thy c + fun check_args (syntax as (n, _)) = if n > Code.args_number thy c then error ("Too many arguments in syntax for constant " ^ quote c) else syntax; in case raw_syn diff -r 1984af09eb41 -r 683b5e3b31fc src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Jul 08 06:43:30 2009 +0200 @@ -627,8 +627,8 @@ fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty; val tys = arg_types num_args (snd c_ty); val ty = nth tys t_pos; - fun mk_constr c t = let val n = Code.no_args thy c - in ((c, arg_types (Code.no_args thy c) (fastype_of t) ---> ty), n) end; + fun mk_constr c t = let val n = Code.args_number thy c + in ((c, arg_types n (fastype_of t) ---> ty), n) end; val constrs = if null case_pats then [] else map2 mk_constr case_pats (nth_drop t_pos ts); fun casify naming constrs ty ts = diff -r 1984af09eb41 -r 683b5e3b31fc src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Jul 08 06:42:35 2009 +0200 +++ b/src/Tools/nbe.ML Wed Jul 08 06:43:30 2009 +0200 @@ -393,10 +393,11 @@ let val ts' = take_until is_dict ts; val c = const_of_idx idx; - val (_, T) = Code.default_typscheme thy c; - val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T; + val T = map_type_tvar (fn ((v, i), _) => + TypeInfer.param typidx (v ^ string_of_int i, [])) + (Sign.the_const_type thy c); val typidx' = typidx + 1; - in of_apps bounds (Term.Const (c, T'), ts') typidx' end + in of_apps bounds (Term.Const (c, T), ts') typidx' end | of_univ bounds (BVar (n, ts)) typidx = of_apps bounds (Bound (bounds - n - 1), ts) typidx | of_univ bounds (t as Abs _) typidx =