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.
more antiquotations
authorhaftmann
Mon, 14 Sep 2009 08:36:58 +0200
changeset 32569 c4c12ef9d4d1
parent 32568 89518a3074e1
child 32570 8df26038caa9
more antiquotations
src/HOL/Tools/Function/fundef_core.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Function/fundef_core.ML	Mon Sep 14 08:36:57 2009 +0200
+++ b/src/HOL/Tools/Function/fundef_core.ML	Mon Sep 14 08:36:58 2009 +0200
@@ -478,7 +478,7 @@
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
     let
       val f_def =
-          Abs ("x", domT, Const ("FunDef.THE_default", ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
+          Abs ("x", domT, Const (@{const_name FunDef.THE_default}, ranT --> (ranT --> boolT) --> ranT) $ (default $ Bound 0) $
                                 Abs ("y", ranT, G $ Bound 1 $ Bound 0))
               |> Syntax.check_term lthy
 
@@ -767,7 +767,7 @@
       val R' = Free ("R", fastype_of R)
 
       val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
-      val inrel_R = Const ("FunDef.in_rel", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
+      val inrel_R = Const (@{const_name FunDef.in_rel}, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
       val wfR' = cterm_of thy (HOLogic.mk_Trueprop (Const (@{const_name "Wellfounded.wfP"}, (domT --> domT --> boolT) --> boolT) $ R')) (* "wf R'" *)
isabelle