Do not register pre-datatype MRBNFs

ISSUES FIXED: #121

Author: jvanbruegge

Tools/mrbnf_comp.ML

@@ -1431,7 +1431,6 @@ fun seal_mrbnf qualify (unfold_set : unfold_set) b force_out_of_line Ds all_Ds m
       |> map (fn (b, def) => ((b, []), [([def], [])]))
     val (noted, lthy'') = lthy'
       |> Local_Theory.notes notes
-      ||> (if repTA = TA then I else register_mrbnf_raw (fst (dest_Type TA)) mrbnf'')
   in
     ((morph_mrbnf (substitute_noted_thm noted) mrbnf'', the info_opt, (all_Ds, absT_info)), lthy'')
   end;

case_studies/Pi_Calculus/Commitment.thy

@@ -84,7 +84,7 @@ abbreviation "bvars \<equiv> bns"
 abbreviation "fvars \<equiv> fns"
 
 lemma bns_bound: "|bns \<alpha>| <o |UNIV::'a::var set|"
-  by (cases \<alpha>) (auto simp: emp_bound infinite_UNIV)
+  by (cases \<alpha>) auto
 
 local_setup \<open>Binder_Sugar.register_binder_sugar "Commitment.commit" {
   ctors = [
@@ -111,7 +111,7 @@ local_setup \<open>Binder_Sugar.register_binder_sugar "Commitment.commit" {
   pset_ctors = [],
   strong_induct = NONE,
   inject = @{thms commit.inject},
-  mrbnf = the (MRBNF_Def.mrbnf_of @{context} "Commitment.commit_pre"),
+  mrbnf = #mrbnf (the (Binder_Sugar.binder_sugar_of @{context} @{type_name commit})),
   set_simpss = [],
   subst_simps = NONE,
   IImsupp_Diffs = NONE,

operations/Composition.thy

@@ -75,6 +75,9 @@ let
   val ((mrbnf2, _, (Ds, info)), lthy) = MRBNF_Comp.seal_mrbnf I (snd accum) (Binding.name (name2 ^ "_pre")) true (fst tys2) [] mrbnf2 NONE lthy
   val _ = @{print} "seal2"
 
+  val lthy = MRBNF_Def.register_mrbnf_raw "Composition.T1_pre" mrbnf1 lthy
+  val lthy = MRBNF_Def.register_mrbnf_raw "Composition.T2_pre" mrbnf2 lthy
+
   (* Step 3: Register the pre-MRBNF as a BNF in its live variables *)
   val (bnf1, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf1 lthy
   val (bnf2, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf2 lthy

operations/Greatest_Fixpoint.thy

@@ -46,6 +46,8 @@ local_setup \<open>fn lthy =>
   val ((mrbnf1, _, (Ds, info)), lthy) = MRBNF_Comp.seal_mrbnf I (snd accum) (Binding.name (name1 ^ "_pre")) true (fst tys1) [] mrbnf1 NONE lthy
   val _ = @{print} "seal"
 
+  val lthy = MRBNF_Def.register_mrbnf_raw "Greatest_Fixpoint.term_pre" mrbnf1 lthy;
+
   (* Step 3: Register the pre-MRBNF as a BNF in its live variables *)
   val (bnf1, lthy) = MRBNF_Def.register_mrbnf_as_bnf mrbnf1 lthy
   val _ = @{print} "register"