Fix previous fix for passive positions

jvanbruegge · Dec 24, 2024 · a0c3fc9 · a0c3fc9
1 parent 4650416
commit a0c3fc9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Tools/mrbnf_fp.ML b/Tools/mrbnf_fp.ML
@@ -1799,7 +1799,7 @@ fun construct_binder_fp fp_kind mrbnf_ks binding_relation lthy =
     ))) zs FVarsss;
 
     val (UNIV_T, _) = lthy
-      |> fold Variable.declare_typ (map (body_type o fastype_of) fs)
+      |> fold Variable.declare_typ (map (body_type o fastype_of) fs @ passives)
       |> apfst hd o mk_TFrees' [Type.sort_of_atyp (body_type (fastype_of (hd fs)))];
 
     val FVars_bds = mk_bd_thms (MRBNF_Def.bd_of_mrbnf (hd mrbnfs)) (flat FVars_raw_bds);