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/Function/fun.ML
changeset 67149 e61557884799
parent 63352 4eaf35781b23 
--- a/src/HOL/Tools/Function/fun.ML	Wed Dec 06 19:34:59 2017 +0100
+++ b/src/HOL/Tools/Function/fun.ML	Wed Dec 06 20:43:09 2017 +0100
@@ -70,7 +70,7 @@
         val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
       in
         HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
-          Const (@{const_name undefined}, rT))
+          Const (\<^const_name>\<open>undefined\<close>, rT))
         |> HOLogic.mk_Trueprop
         |> fold_rev Logic.all qs
       end
@@ -171,7 +171,7 @@
 
 
 val _ =
-  Outer_Syntax.local_theory' @{command_keyword fun}
+  Outer_Syntax.local_theory' \<^command_keyword>\<open>fun\<close>
     "define general recursive functions (short version)"
     (function_parser fun_config
       >> (fn (config, (fixes, specs)) => add_fun_cmd fixes specs config))
isabelle