304     val insts = (map o map) SOME arg_namess 

   304     val insts = (map o map) SOME arg_namess 

   305    

   305    

   306     val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt

   306     val ([p_name], ctxt') = Variable.variant_fixes ["p"] ctxt

   307     val p = Free (p_name, @{typ perm})

   307     val p = Free (p_name, @{typ perm})

   308 

   308 

   309     val acc_prems = 

   310     val acc_prems = 

   310      map prop_of induct_thms

   311      map prop_of induct_thms

   311      |> map2 forall_elim_list argss 

   312      |> map2 forall_elim_list argss 

   312      |> map (strip_qnt_body "all")

   313      |> map (strip_qnt_body "all")

   313      |> map (curry Logic.nth_prem 1)

   314      |> map (curry Logic.nth_prem 1)