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.
compile
authorblanchet
Mon, 03 Mar 2014 12:48:20 +0100
changeset 55861 0a8200e31474
parent 55860 756275b550d9
child 55862 b458558cbcc2
compile
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Mar 03 12:48:20 2014 +0100
@@ -523,7 +523,7 @@
     lthy =
   let
     val nn = length fpTs;
-    val fpTs = range_type (snd (strip_typeN nn (fastype_of (co_rec_of dtor_coiters))));
+    val fpT = range_type (snd (strip_typeN nn (fastype_of (co_rec_of dtor_coiters))));
 
     fun generate_coiter pre ((pfss, cqfsss), f_absTs) dtor_coiter =
       (mk_binding pre,
isabelle