author | haftmann |
Tue, 31 Oct 2006 09:28:57 +0100 | |
changeset 21114 | 3c09ec7565ed |
parent 21113 | 5b76e541cc0a |
child 21115 | f4e79a09c305 |
--- a/src/HOL/Extraction/Higman.thy Tue Oct 31 09:28:56 2006 +0100 +++ b/src/HOL/Extraction/Higman.thy Tue Oct 31 09:28:57 2006 +0100 @@ -337,7 +337,7 @@ end; *} -code_gen good_prefix (SML -) +(*code_gen good_prefix (SML "~/gen_code/higman.ML") ML {* local @@ -383,6 +383,6 @@ val xs4 = good_prefix f2; end; -*} +*}*) end