Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/BNF/Tools/bnf_comp.ML
changeset 49835 31f32ec4d766
parent 49833 1d80798e8d8a
child 50059 a292751fb345 
--- a/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 18:58:20 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Fri Oct 12 21:22:35 2012 +0200
@@ -625,7 +625,7 @@
     val deads = map TFree params;
 
     val ((bdT_name, (bdT_glob_info, bdT_loc_info)), lthy) =
-      typedef NONE (bdT_bind, params, NoSyn)
+      typedef (bdT_bind, params, NoSyn)
         (HOLogic.mk_UNIV bd_repT) NONE (EVERY' [rtac exI, rtac UNIV_I] 1) lthy;
 
     val bnf_bd' = mk_dir_image bnf_bd
isabelle