# HG changeset patch
# User wenzelm
# Date 938803058 -7200
# Node ID c859160e78b05980add2c28ce296b1e59fd56a8f
# Parent  99305245f6bd04ccf726256ee1db34414143aac2
added atomic_thesis;

diff -r 99305245f6bd -r c859160e78b0 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Fri Oct 01 20:36:53 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Fri Oct 01 20:37:38 1999 +0200
@@ -3,19 +3,26 @@
     Author:     Markus Wenzel, TU Muenchen
 
 Automatic term bindings -- logic specific patterns.
+
+The implementation below works fine with the more common
+object-logics, such as HOL, ZF.
 *)
 
 signature AUTO_BIND =
 sig
   val goal: term -> (indexname * term option) list
   val facts: string -> term list -> (indexname * term option) list
+  val atomic_thesis: term -> (string * term) * term
 end;
 
 structure AutoBind: AUTO_BIND =
 struct
 
+val thesisN = "thesis";
+val thisN = "this";
 
-(* goals *)
+
+(* goal *)
 
 fun statement_binds (name, prop) =
   let
@@ -27,7 +34,7 @@
       (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
   in map (fn (s, t) => ((s, 0), t)) env end;
 
-fun goal prop = statement_binds ("thesis", prop);
+fun goal prop = statement_binds (thesisN, prop);
 
 
 (* facts *)
@@ -39,7 +46,15 @@
 fun facts _ [] = []
   | facts name props =
       let val prop = Library.last_elem props
-      in dddot_bind prop @ statement_binds ("this", prop) end;
+      in dddot_bind prop @ statement_binds (thisN, prop) end;
+
+
+(* atomic_thesis *)
+
+fun mk_free t = Free (thesisN, Term.fastype_of t);
+
+fun atomic_thesis ((c as Const ("Trueprop", _)) $ t) = ((thesisN, t), c $ mk_free t)
+  | atomic_thesis t = ((thesisN, t), mk_free t);
       
 
 end;