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/Transfer/transfer_bnf.ML
changeset 58177 166131276380
parent 57890 1e13f63fb452
child 58179 2de7b0313de3 
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Sep 03 22:47:48 2014 +0200
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML	Wed Sep 03 22:49:05 2014 +0200
@@ -291,7 +291,8 @@
   end
 
 val _ = Context.>> (Context.map_theory (bnf_interpretation
-  (bnf_only_type_ctr (fn bnf => map_local_theory (transfer_bnf_interpretation bnf)))))
+  (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation))
+  (bnf_only_type_ctr (transfer_bnf_interpretation))))
 
 (* simplification rules for the predicator *)
 
@@ -360,7 +361,8 @@
     snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy)
   end
 
-val _ = Context.>> (Context.map_theory (fp_sugar_interpretation (fp_sugar_only_type_ctr
-  (fn fp_sugars => map_local_theory (fold transfer_fp_sugar_interpretation fp_sugars)))))
+val _ = Context.>> (Context.map_theory (fp_sugar_interpretation
+  (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation))
+  (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation))))
 
 end
isabelle