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_fun.ML
changeset 80636 4041e7c8059d
parent 74561 8e6c973003c8 
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Sun Aug 04 17:39:47 2024 +0200
@@ -39,7 +39,7 @@
 fun pred_of_function thy name =
   (case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
     [] => NONE
-  | [(_, p)] => SOME (fst (dest_Const p))
+  | [(_, p)] => SOME (dest_Const_name p)
   | _ => error ("Multiple matches possible for lookup of constant " ^ name))
 
 fun defined_const thy name = is_some (pred_of_function thy name)
@@ -87,8 +87,8 @@
     end;
 
 fun keep_functions thy t =
-  (case try dest_Const (fst (strip_comb t)) of
-    SOME (c, _) => Predicate_Compile_Data.keep_function thy c
+  (case try dest_Const_name (fst (strip_comb t)) of
+    SOME c => Predicate_Compile_Data.keep_function thy c
   | _ => false)
 
 fun flatten thy lookup_pred t (names, prems) =
isabelle