# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1531747446 -7200
# Node ID d812b6ee711bd14b0d3aa64c6676603345cdb670
# Parent  4a2b72b082dc12912be019c01a667e6b44c160e1
Made simproc for sqrt/root of numeral more robust

diff -r 4a2b72b082dc -r d812b6ee711b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Jul 16 08:32:27 2018 +0200
+++ b/src/HOL/Transcendental.thy	Mon Jul 16 15:24:06 2018 +0200
@@ -7199,6 +7199,7 @@
         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
@@ -7212,6 +7213,8 @@
           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
@@ -7233,6 +7236,8 @@
             SOME (@{thm transitive} OF [eq_thm, thm])
           end
   end
+    handle TERM _ => NONE
+         | Match => NONE
 
 end
 \<close>