# 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