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/coinduction.ML
changeset 81954 6f2bcdfa9a19
parent 81942 da3c3948a39c 
--- a/src/HOL/Tools/coinduction.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/coinduction.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -71,7 +71,7 @@
             val (instT, inst) = Thm.match (thm_concl, concl);
             val rhoTs = map (fn (v, T) => (TVar v, Thm.typ_of T)) (TVars.dest instT);
             val rhots = map (fn (v, t) => (Var v, Thm.term_of t)) (Vars.dest inst);
-            val xs = hd (Thm.prems_of raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
+            val xs = hd (Thm.take_prems_of 1 raw_thm) |> HOLogic.dest_Trueprop |> strip_comb |> snd
               |> map (subst_atomic_types rhoTs);
             val raw_eqs = map (fn x => (x, AList.lookup op aconv rhots x |> the)) xs;
             val ((names, ctxt), Ts) = map_split (apfst fst o dest_Var o fst) raw_eqs
isabelle