# HG changeset patch
# User wenzelm
# Date 972926738 -3600
# Node ID 445e3b87f28bab40ad996a6920c96b07e3026f1b
# Parent  ef2a753cda2a5d1c16dabcbf53d7379685c78db5
improved statement bindings for props;
tuned;

diff -r ef2a753cda2a -r 445e3b87f28b src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Mon Oct 30 18:25:10 2000 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Mon Oct 30 18:25:38 2000 +0100
@@ -3,64 +3,33 @@
     Author:     Markus Wenzel, TU Muenchen
     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
-Automatic term bindings -- logic specific patterns.
+Logic specific patterns and automatic term bindings.
 
 Note: the current implementation is not quite 'generic', but works
-fine with the more common object-logics (HOL, FOL, ZF etc.).
+fine with common object-logics (HOL, FOL, ZF etc.).
 *)
 
 signature AUTO_BIND =
 sig
+  val is_judgment: term -> bool
+  val add_judgment: bstring * string * mixfix -> theory -> theory
+  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
   val goal: term -> (indexname * term option) list
   val facts: string -> term list -> (indexname * term option) list
   val thesisN: string
-  val is_judgment: term -> bool
-  val add_judgment: bstring * string * mixfix -> theory -> theory
-  val add_judgment_i: bstring * typ * mixfix -> theory -> theory
 end;
 
 structure AutoBind: AUTO_BIND =
 struct
 
-val thesisN = "thesis";
-val thisN = "this";
-
-
-(** bindings **)
-
-fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
-
-
-(* goal *)
-
-fun statement_binds (name, prop) =
-  let
-    val concl = Logic.strip_assums_concl prop;
-    val parms = Logic.strip_params prop;
-
-    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs parms concl)),
-      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs parms t) | _ => None)];
-  in map (fn (s, t) => ((s, 0), t)) env end;
-
-fun goal prop = statement_binds (thesisN, prop);
-
-
-(* facts *)
-
-fun get_subject prop =
-  (case (Logic.strip_assums_concl prop) of
-    Const ("Trueprop", _) $ (_ $ t) => Some (list_abs (Logic.strip_params prop) t)
-  | _ => None);
-
-fun facts _ [] = []
-  | facts name props =
-      let val prop = Library.last_elem props
-      in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end;
-
-
 
 (** judgments **)
 
+fun strip_judgment prop =
+  (case (Logic.strip_assums_concl prop) of
+    Const ("Trueprop", _) $ t => t
+  | t => t);
+
 fun is_judgment (Const ("Trueprop", _) $ _) = true
   | is_judgment _ = false;
 
@@ -74,4 +43,33 @@
 val add_judgment_i = gen_add_judgment Theory.add_consts_i;
 
 
+
+(** bindings **)
+
+val thesisN = "thesis";
+val thisN = "this";
+
+fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
+
+fun statement_binds name prop =
+  [((name, 0), Some (list_abs (Logic.strip_params prop) (strip_judgment prop)))];
+
+
+(* goal *)
+
+fun goal prop = statement_binds thesisN prop;
+
+
+(* facts *)
+
+fun get_arg prop =
+  (case strip_judgment prop of
+    _ $ t => Some (list_abs (Logic.strip_params prop) t)
+  | _ => None);
+
+fun facts _ [] = []
+  | facts name props =
+      let val prop = Library.last_elem props
+      in [(Syntax.dddot_indexname, get_arg prop)] @ statement_binds thisN prop end;
+
 end;