# HG changeset patch # User blanchet # Date 1383558761 -3600 # Node ID 6d64669184ae6dbbe0d8cba126aa038d6a72a4c0 # Parent e039a9b9700def80c11ef3b8759d222a05152847 conceal definition diff -r e039a9b9700d -r 6d64669184ae src/HOL/BNF/Tools/bnf_fp_n2m.ML --- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Sat Nov 02 17:50:28 2013 +0100 +++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Mon Nov 04 10:52:41 2013 +0100 @@ -23,7 +23,7 @@ open BNF_FP_N2M_Tactics fun force_typ ctxt T = - map_types Type_Infer.paramify_vars + map_types Type_Infer.paramify_vars #> Type.constraint T #> Syntax.check_term ctxt #> singleton (Variable.polymorphic ctxt); @@ -224,7 +224,7 @@ fun mk_s TU' = let val i = find_index (fn T => co_alg_argT TU' = T) Xs; - val sF = co_alg_funT TU'; + val sF = co_alg_funT TU'; val F = nth iter_preTs i; val s = nth iter_strs i; in @@ -238,7 +238,7 @@ |> force_typ names_lthy smapT |> hidden_to_unit; val smap_argTs = strip_typeN live (fastype_of smap) |> fst; - fun mk_smap_arg TU = + fun mk_smap_arg TU = (if domain_type TU = range_type TU then HOLogic.id_const (domain_type TU) else if is_rec then @@ -265,7 +265,7 @@ in (case b_opt of NONE => ((t, Drule.dummy_thm), lthy) - | SOME b => Local_Theory.define ((b, NoSyn), ((Thm.def_binding b, []), + | SOME b => Local_Theory.define ((b, NoSyn), ((Binding.conceal (Thm.def_binding b), []), fold_rev Term.absfree (if is_rec then rec_strs' else fold_strs') t)) lthy |>> apsnd snd) end;