# HG changeset patch # User haftmann # Date 1162560158 -3600 # Node ID e979928961703192593846404ff78897ffdba4ef # Parent 25bd46916c1220b46478ca42043e61a880465719 added code gen II diff -r 25bd46916c12 -r e97992896170 src/HOL/Extraction/Higman.thy --- a/src/HOL/Extraction/Higman.thy Fri Nov 03 14:22:37 2006 +0100 +++ b/src/HOL/Extraction/Higman.thy Fri Nov 03 14:22:38 2006 +0100 @@ -337,7 +337,7 @@ end; *} -(*code_gen good_prefix (SML "~/gen_code/higman.ML") +code_gen good_prefix (SML *) ML {* local @@ -383,6 +383,6 @@ val xs4 = good_prefix f2; end; -*}*) +*} end