1.1 --- a/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:36 2007 +0200
     1.2 +++ b/src/HOL/Complex/ex/ReflectedFerrack.thy	Mon Aug 13 21:22:37 2007 +0200
     1.3 @@ -1993,7 +1993,7 @@
     1.4    "ferrack_test u = linrqe (A (A (Imp (Lt (Sub (Bound 1) (Bound 0)))
     1.5      (E (Eq (Sub (Add (Bound 0) (Bound 2)) (Bound 1)))))))"
     1.6  
     1.7 -code_gen linrqe ferrack_test in SML to Ferrack
     1.8 +code_gen linrqe ferrack_test in SML module_name Ferrack
     1.9  
    1.10  (*code_module Ferrack
    1.11    contains