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/Tools/BNF/bnf_gfp_rec_sugar.ML
changeset 62698 9d706e37ddab
parent 62686 6e8924f957f6
child 63064 2f18172214c8 
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 13:32:40 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Tue Mar 22 13:44:50 2016 +0100
@@ -1455,7 +1455,7 @@
                     val (distincts, discIs, _, split_sels, split_sel_asms) =
                       case_thms_of_term lthy raw_rhs;
 
-                    val raw_code_thm = 
+                    val raw_code_thm =
                       Goal.prove_sorry lthy [] [] raw_goal
                         (fn {context = ctxt, prems = _} =>
                           mk_primcorec_raw_code_tac ctxt distincts discIs split_sels split_sel_asms
isabelle