# HG changeset patch
# User blanchet
# Date 1348761275 -7200
# Node ID 0e248756147a4ad114cd4c18eb24fa493c132919
# Parent  29be73b789f920ab4f6f9ba2d3e644d4307a59ff
repaired signature

diff -r 29be73b789f9 -r 0e248756147a src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 17:00:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Sep 27 17:54:35 2012 +0200
@@ -20,7 +20,7 @@
       (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
     (term list * term list list * thm * thm list * thm list * thm list * thm list list * thm list *
      thm list list) * local_theory
-  val parse_wrap_options: (bool * bool) parser
+  val parse_wrap_options: bool parser
   val parse_bound_term: (binding * string) parser
 end;