
diff -r 93d1ad7662a9 -r 6407d832da03 src/HOL/Complex/ex/ReflectedFerrack.thy
--- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Thu Jun 28 19:09:43 2007 +0200
+++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Fri Jun 29 16:05:00 2007 +0200
@@ -2004,7 +2004,6 @@
 
 ML {* Ferrack.ReflectedFerrack.ferrack_test () *}
 
-code_gen linrqe ferrack_test in SML file "~~/../../gen_code/ferrack.ML"
 use "linreif.ML"
 oracle linr_oracle ("term") = ReflectedFerrack.linrqe_oracle
 use"linrtac.ML"




