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/core_data.ML
changeset 81954 6f2bcdfa9a19
parent 80636 4041e7c8059d 
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -237,7 +237,7 @@
         val prems2 = maps (dest_conjunct_prem o rewrite_rule ctxt2 tuple_rew_rules) prems1
         val pats =
           map (swap o HOLogic.dest_eq o HOLogic.dest_Trueprop)
-            (take nargs (Thm.prems_of case_th))
+            (Thm.take_prems_of nargs case_th)
         val case_th' =
           Thm.instantiate (TVars.empty, Vars.make (inst_of_matches pats)) case_th
             OF replicate nargs @{thm refl}
@@ -325,7 +325,7 @@
 
 fun set_elim thm =
   let
-    val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))))
+    val name = dest_Const_name (fst (strip_comb (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm)))))
   in
     PredData.map (Graph.map_node name (map_pred_data (apsnd (apfst (apfst (apsnd (K (SOME thm))))))))
   end
isabelle