dropped local cg cmd
authorhaftmann
Fri, 29 Jun 2007 16:05:00 +0200
changeset 23518 6407d832da03
parent 23517 93d1ad7662a9
child 23519 a4ffa756d8eb
dropped local cg cmd
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"