src/HOL/BNF/Tools/bnf_def.ML
changeset 54156 a8cf84bfa9be
parent 54045 369a4a14583a
child 54158 0af35cebe8ca
equal deleted inserted replaced
54155:b964fad0cbbd 54156:a8cf84bfa9be
   631           Type (C, Ts) => if forall (can dest_TFree) Ts
   631           Type (C, Ts) => if forall (can dest_TFree) Ts
   632             then (Binding.qualified_name C, C) else err bd_rhsT
   632             then (Binding.qualified_name C, C) else err bd_rhsT
   633         | T => err T)
   633         | T => err T)
   634       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
   634       else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
   635 
   635 
   636     val def_qualify = Binding.qualify false (Binding.name_of bnf_b);
   636     val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
   637 
   637 
   638     fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
   638     fun mk_suffix_binding suf = Binding.suffix_name ("_" ^ suf) bnf_b;
   639 
   639 
   640     fun maybe_define user_specified (b, rhs) lthy =
   640     fun maybe_define user_specified (b, rhs) lthy =
   641       let
   641       let