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/inductive_realizer.ML
changeset 81954 6f2bcdfa9a19
parent 80636 4041e7c8059d 
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jan 22 21:35:05 2025 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jan 22 22:22:19 2025 +0100
@@ -372,7 +372,7 @@
       let
         val vs' = rename (map (apply2 (fst o fst o dest_Var))
           (params ~~ List.take (snd (strip_comb (HOLogic.dest_Trueprop
-            (hd (Thm.prems_of (hd inducts))))), nparms))) vs;
+            (hd (Thm.take_prems_of 1 (hd inducts))))), nparms))) vs;
         val rs = indrule_realizer thy induct raw_induct rsets params'
           (vs' @ Ps) rec_names rss' intrs dummies;
         val rlzs = map (fn (r, ind) => Extraction.realizes_of thy (vs' @ Ps) r
@@ -505,7 +505,7 @@
     fun err () = error "ind_realizer: bad rule";
     val sets =
       (case HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of thm)) of
-           [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.prems_of thm)))]
+           [_] => [pred_of (HOLogic.dest_Trueprop (hd (Thm.take_prems_of 1 thm)))]
          | xs => map (pred_of o fst o HOLogic.dest_imp) xs)
          handle TERM _ => err () | List.Empty => err ();
   in
isabelle