--- a/src/Pure/thm.ML Thu Jul 05 20:01:37 2007 +0200
+++ b/src/Pure/thm.ML Thu Jul 05 20:01:38 2007 +0200
@@ -35,11 +35,12 @@
val cterm_of: theory -> term -> cterm
val ctyp_of_term: cterm -> ctyp
- type tag (* = string * string list *)
+ type tag = string * string list
(*meta theorems*)
type thm
- type attribute (* = Context.generic * thm -> Context.generic * thm *)
+ type conv = cterm -> thm
+ type attribute = Context.generic * thm -> Context.generic * thm
val rep_thm: thm ->
{thy: theory,
der: bool * Proofterm.proof,
@@ -88,9 +89,9 @@
val reflexive: cterm -> thm
val symmetric: thm -> thm
val transitive: thm -> thm -> thm
- val beta_conversion: bool -> cterm -> thm
- val eta_conversion: cterm -> thm
- val eta_long_conversion: cterm -> thm
+ val beta_conversion: bool -> conv
+ val eta_conversion: conv
+ val eta_long_conversion: conv
val abstract_rule: string -> cterm -> thm -> thm
val combination: thm -> thm -> thm
val equal_intr: thm -> thm -> thm
@@ -238,7 +239,7 @@
in Cterm {thy_ref = Theory.self_ref thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
- Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise TERM (msg, [t1, t2]);
+ Theory.merge_refs (r1, r2);
(* destructors *)
@@ -368,6 +369,8 @@
prop: term} (*conclusion*)
with
+type conv = cterm -> thm;
+
(*attributes subsume any kind of rules or context modifiers*)
type attribute = Context.generic * thm -> Context.generic * thm;
@@ -409,10 +412,10 @@
(* merge theories of cterms/thms; raise exception if incompatible *)
fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm {thy_ref = r2, ...}) =
- Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th]);
+ Theory.merge_refs (r1, r2);
fun merge_thys2 (th1 as Thm {thy_ref = r1, ...}) (th2 as Thm {thy_ref = r2, ...}) =
- Theory.merge_refs (r1, r2) handle TERM (msg, _) => raise THM (msg, 0, [th1, th2]);
+ Theory.merge_refs (r1, r2);
(* basic components *)