# 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;