| changeset 23810 | f5e6932d0500 |
| parent 23747 | b07cff284683 |
| child 24221 | dd4a7ea0e64a |
--- a/src/HOL/Extraction/Higman.thy Mon Jul 16 09:29:02 2007 +0200 +++ b/src/HOL/Extraction/Higman.thy Mon Jul 16 09:29:03 2007 +0200 @@ -409,12 +409,11 @@ arbitrary_LT \<equiv> arbitrary_LT' arbitrary_TT \<equiv> arbitrary_TT' -code_gen higman_idx in SML +code_gen higman_idx in SML to Higman ML {* local - open ROOT.Higman - open ROOT.Nat + open Higman in val a = 16807.0;