--- 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
--- 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]
: