--- 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;