Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
run type inference on input to wrap_data
authortraytel
Thu, 11 Apr 2013 16:39:01 +0200
changeset 51696 745a074246c2
parent 51695 876281e7642f
child 51697 1ce319118d59
run type inference on input to wrap_data
src/HOL/BNF/Tools/bnf_wrap.ML file | annotate | diff | comparison | revisions 
--- 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 "]"};
isabelle