src/HOL/Tools/inductive_realizer.ML

 
     fun add_ind_realizer Ps thy =
       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
           (Thm.prop_of ind)) (rs ~~ inducts);
         val used = fold Term.add_free_names rlzs [];

 fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.mapping
   let
     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 
     add_ind_realizers (hd sets)
       (case arg of