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/Predicate_Compile/predicate_compile_core.ML
changeset 79336 032a31db4c6f
parent 70308 7f568724d67e 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 22 17:19:08 2023 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Dec 22 21:03:16 2023 +0100
@@ -1144,9 +1144,9 @@
             (list_comb (Const (name, T), args))))
         val lhs = Const (mode_cname, funT)
         val def = Logic.mk_equals (lhs, predterm)
-        val ([definition], thy') = thy |>
+        val (definition, thy') = thy |>
           Sign.add_consts [(Binding.name mode_cbasename, funT, NoSyn)] |>
-          Global_Theory.add_defs false [((Binding.name (Thm.def_name mode_cbasename), def), [])]
+          Global_Theory.add_def (Binding.name (Thm.def_name mode_cbasename), def)
         val ctxt' = Proof_Context.init_global thy'
         val rules as ((intro, elim), _) =
           create_intro_elim_rule ctxt' mode definition mode_cname funT (Const (name, T))
isabelle