src/HOL/Tools/smallvalue_generators.ML

       "Creation of smallvalue generators failed because the datatype contains a function type";
     thy)
 
 (** building and compiling generator expressions **)
 
-structure Counterexample = Proof_Data (
+structure Counterexample = Proof_Data
+(
   type T = unit -> int -> term list option
+  (* FIXME avoid user error with non-user text *)
   fun init _ () = error "Counterexample"
 );
 val put_counterexample = Counterexample.put;
 
 val target = "Quickcheck";