# HG changeset patch
# User haftmann
# Date 1162283337 -3600
# Node ID 3c09ec7565edfd6283d77f8ca3c4d0c0907e4ee5
# Parent  5b76e541cc0afd8ea2f9813de4066aec99c31de0
disabled some code generation (an intermeidate solution)

diff -r 5b76e541cc0a -r 3c09ec7565ed src/HOL/Extraction/Higman.thy
--- 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