src/HOL/Extraction/Higman.thy

   [symmetric, code inline]: "arbitrary_TT = arbitrary"
 
 code_datatype L0 L1 arbitrary_LT
 code_datatype T0 T1 T2 arbitrary_TT
 
-code_gen higman_idx in SML module_name Higman
+export_code higman_idx in SML module_name Higman
 
 ML {*
 local
   open Higman
 in