| changeset 24348 | c708ea5b109a |
| parent 24249 | 1f60b45c5f97 |
| child 25417 | ddb060d37ca8 |
--- a/src/HOL/Extraction/Higman.thy Mon Aug 20 18:07:31 2007 +0200 +++ b/src/HOL/Extraction/Higman.thy Mon Aug 20 18:07:49 2007 +0200 @@ -427,7 +427,7 @@ 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