# HG changeset patch
# User wenzelm
# Date 1737470919 -3600
# Node ID d25181c1807a36c0fb0794a8c0b5dfaeb046d6dd
# Parent  372ff330a9d95d22dbe4ba8458084d4492a55cd7
clarified exceptions;

diff -r 372ff330a9d9 -r d25181c1807a src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jan 21 00:01:31 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 15:48:39 2025 +0100
@@ -55,7 +55,7 @@
 
 (* basic logic *)
 
-fun implies_elim_all th = implies_elim_list th (map Thm.assume (cprems_of th))
+fun implies_elim_all th = implies_elim_list th (map Thm.assume_cterm (cprems_of th))
 
 fun meta_mp th1 th2 =
   let
@@ -122,7 +122,7 @@
     val th1b = Thm.implies_intr th2c th1a
     val th2b = Thm.implies_intr th1c th2a
     val i = Thm.instantiate' [] [SOME (Thm.dest_arg th1c), SOME (Thm.dest_arg th2c)] @{thm iffI}
-    val i1 = Thm.implies_elim i (Thm.assume (Thm.cprop_of th2b))
+    val i1 = Thm.implies_elim i (Thm.assume_cterm (Thm.cprop_of th2b))
     val i2 = Thm.implies_elim i1 th1b
     val i3 = Thm.implies_intr (Thm.cprop_of th2b) i2
     val i4 = Thm.implies_elim i3 th2b
diff -r 372ff330a9d9 -r d25181c1807a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jan 21 00:01:31 2025 +0100
+++ b/src/Pure/thm.ML	Tue Jan 21 15:48:39 2025 +0100
@@ -142,7 +142,8 @@
   val extern_oracles: bool -> Proof.context -> (Markup.T * xstring) list
   val check_oracle: Proof.context -> xstring * Position.T -> string
   (*inference rules*)
-  val assume: cterm -> thm
+  val assume: cterm -> thm  (*exception THM*)
+  val assume_cterm: cterm -> thm  (*exception CTERM*)
   val implies_intr: cterm -> thm -> thm
   val implies_elim: thm -> thm -> thm
   val forall_intr: cterm -> thm -> thm
@@ -1262,6 +1263,10 @@
       end
   end;
 
+fun assume_cterm A = assume A
+  handle THM (msg, _, _) => raise CTERM (msg, [A]);
+
+
 (*Implication introduction
     [A]
      :