# HG changeset patch
# User haftmann
# Date 1183125900 -7200
# Node ID 6407d832da037142b7b1548e52b5cc69914fcd1a
# Parent  93d1ad7662a9e0e457bd9053c2abacf5d4015197
dropped local cg cmd

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"