# HG changeset patch
# User traytel
# Date 1365691141 -7200
# Node ID 745a074246c283271836071aba96e81ae889a8ad
# Parent  876281e7642f23680ac21feaf635841326cfecaa
run type inference on input to wrap_data

diff -r 876281e7642f -r 745a074246c2 src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 16:03:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 16:39:01 2013 +0200
@@ -655,7 +655,7 @@
 
 val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
   Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
-  prepare_wrap_datatype Syntax.parse_term;
+  prepare_wrap_datatype Syntax.read_term;
 
 fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --|  @{keyword "]"};