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/HOLCF/Tools/cpodef.ML
changeset 74305 28a582aa25dd
parent 69829 3bfa28b3a5b2 
--- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Sep 12 20:52:39 2021 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Sep 12 22:31:51 2021 +0200
@@ -53,10 +53,10 @@
 
 (* building terms *)
 
-fun adm_const T = Const (\<^const_name>\<open>adm\<close>, (T --> HOLogic.boolT) --> HOLogic.boolT)
+fun adm_const T = \<^Const>\<open>adm T\<close>
 fun mk_adm (x, T, P) = adm_const T $ absfree (x, T) P
 
-fun below_const T = Const (\<^const_name>\<open>below\<close>, T --> T --> HOLogic.boolT)
+fun below_const T = \<^Const>\<open>below T\<close>
 
 (* proving class instances *)
 
@@ -229,7 +229,7 @@
     val (newT, oldT, set) = prepare prep_term name typ raw_set thy
 
     val goal_bottom_mem =
-      HOLogic.mk_Trueprop (HOLogic.mk_mem (Const (\<^const_name>\<open>bottom\<close>, oldT), set))
+      HOLogic.mk_Trueprop (HOLogic.mk_mem (\<^Const>\<open>bottom oldT\<close>, set))
 
     val goal_admissible =
       HOLogic.mk_Trueprop (mk_adm ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), set)))
isabelle