Fix build failure caused by HOL API change in ThmSetData

HOL breakage was caused by HOL-Theorem-Prover/HOL@ca1d20c4beebb7
CakeML · Oct 27, 2020 · d979dab · d979dab
1 parent d141a15
commit d979dab
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/characteristic/cfLetAutoLib.sml b/characteristic/cfLetAutoLib.sml
@@ -41,7 +41,7 @@ fun get_frame_thms () = !FRAME_THMS;
 
 fun new_exporter nm add =
     ThmSetData.new_exporter {
-      efns = {add = fn {named_thms,thy} => add thy named_thms,
+      efns = {add = fn {named_thm,thy} => add thy [named_thm],
               remove = fn _ => ()},
       settype = nm
     } |> #export