src/HOL/Transcendental.thy

       NONE => NONE
     | SOME m => 
         SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n])
                   @{thm sqrt_numeral_simproc_aux})
   end
+    handle TERM _ => NONE
 
 fun root_simproc (threshold1, threshold2) ctxt ct =
   let
     val [n, x] = 
       ct |> Thm.term_of |> strip_comb |> snd |> map (dest_comb #> snd #> HOLogic.dest_numeral)

         NONE => NONE
       | SOME m => 
           SOME (Thm.instantiate' [] (map (SOME o Thm.cterm_of ctxt o HOLogic.mk_numeral) [m, n, x])
             @{thm root_numeral_simproc_aux})
   end
+    handle TERM _ => NONE
+         | Match => NONE
 
 fun powr_simproc (threshold1, threshold2) ctxt ct =
   let
     val eq_thm = Conv.try_conv (Conv.rewr_conv @{thm numeral_powr_inverse_eq}) ct
     val ct = Thm.dest_equals_rhs (Thm.cprop_of eq_thm)

               @{thm powr_numeral_simproc_aux}
           in
             SOME (@{thm transitive} OF [eq_thm, thm])
           end
   end
+    handle TERM _ => NONE
+         | Match => NONE
 
 end
 \<close>
 
 end