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/Old_Datatype/old_datatype_aux.ML
changeset 69593 3dda49e08b9d
parent 67713 041898537c19 
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Fri Jan 04 23:22:53 2019 +0100
@@ -115,8 +115,8 @@
 fun split_conj_thm th =
   ((th RS conjunct1) :: split_conj_thm (th RS conjunct2)) handle THM _ => [th];
 
-val mk_conj = foldr1 (HOLogic.mk_binop @{const_name HOL.conj});
-val mk_disj = foldr1 (HOLogic.mk_binop @{const_name HOL.disj});
+val mk_conj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>);
+val mk_disj = foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.disj\<close>);
 
 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
isabelle