| changeset 24249 | 1f60b45c5f97 |
| parent 24221 | dd4a7ea0e64a |
| child 24348 | c708ea5b109a |
--- a/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:36 2007 +0200 +++ b/src/HOL/Extraction/Higman.thy Mon Aug 13 21:22:37 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 to Higman +code_gen higman_idx in SML module_name Higman ML {* local