Hide alpha relation by default

Tools/mrbnf_fp.ML

@@ -28,6 +28,9 @@ open MRBNF_Util
 infix 0 RSS
 fun op RSS (thms, thm) = map (fn x => x RS thm) thms;
 
+fun mk_internal internal ctxt f =
+  if internal andalso not (Config.get ctxt MRBNF_Def.mrbnf_internals) then f else I;
+
 fun define_fp_consts fp_kind mrbnf_ks (binding_relation : (int list * int list) list list) lthy =
   let
     val co = (fp_kind = BNF_Util.Greatest_FP);
@@ -288,9 +291,11 @@ fun define_fp_consts fp_kind mrbnf_ks (binding_relation : (int list * int list)
             replicate (nvars + length pfrees) @{thm supp_id_bound} @ flat (replicate (length pbounds) @{thms bij_id supp_id_bound})
           )
         ) mrbnfs;
-      in Inductive.add_inductive flags
-        (map (fn T => (apfst Binding.name (dest_Free T), NoSyn)) alphas) []
-        (map (pair Binding.empty_atts) intros) monos lthy
+      in lthy
+        |> Local_Theory.map_background_naming (mk_internal true lthy Name_Space.concealed)
+        |> Inductive.add_inductive flags
+          (map (fn T => (apfst Binding.name (dest_Free T), NoSyn)) alphas) []
+          (map (pair Binding.empty_atts) intros) monos
       end;
 
     val (lthy, old_lthy) = `Local_Theory.end_nested lthy;
@@ -2633,4 +2638,4 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =
 
   in (fp_result, lthy) end
 
-end
+end

thys/POPLmark/SystemFSub.thy

@@ -17,7 +17,6 @@ binder_datatype 'a "typ" =
     TyVar 'a
   | Top
   | Fun "'a typ" "'a typ"
-  | Rec "(string, 'a typ) lfset"
   | Forall \<alpha>::'a "'a typ" t::"'a typ" binds \<alpha> in t
 
 declare supp_swap_bound[OF cinfinite_imp_infinite[OF typ.UNIV_cinfinite], simp]