# HG changeset patch
# User wenzelm
# Date 1126642769 -7200
# Node ID 9ea1e21797867ec634f277522d029af9b4383116
# Parent  8b2f56aff711d6b4045db63ca886718c510f7a47
added simple_fact;
generalized no_attributes;

diff -r 8b2f56aff711 -r 9ea1e2179786 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Sep 13 22:19:28 2005 +0200
+++ b/src/Pure/thm.ML	Tue Sep 13 22:19:29 2005 +0200
@@ -139,7 +139,8 @@
   val cabs: cterm -> cterm -> cterm
   val major_prem_of: thm -> term
   val no_prems: thm -> bool
-  val no_attributes: 'a -> 'a * 'b attribute list
+  val no_attributes: 'a -> 'a * 'b list
+  val simple_fact: 'a -> ('a * 'b list) list
   val apply_attributes: ('a * thm) * 'a attribute list -> 'a * thm
   val applys_attributes: ('a * thm list) * 'a attribute list -> 'a * thm list
   val terms_of_tpairs: (term * term) list -> term list
@@ -397,6 +398,7 @@
 type 'a attribute = 'a * thm -> 'a * thm;
   
 fun no_attributes x = (x, []);
+fun simple_fact x = [(x, [])];
 fun apply_attributes (x_th, atts) = Library.apply atts x_th;
 fun applys_attributes (x_ths, atts) = foldl_map (Library.apply atts) x_ths;