# HG changeset patch
# User wenzelm
# Date 935488217 -7200
# Node ID aee8f76fe54cef8c9847bc02279862baacfbb19e
# Parent  109b1ef4686a81e6e6c43da1bedc1d16b0153917
??thesis: include params;

diff -r 109b1ef4686a -r aee8f76fe54c src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Tue Aug 24 11:43:30 1999 +0200
+++ b/src/Pure/Isar/auto_bind.ML	Tue Aug 24 11:50:17 1999 +0200
@@ -19,9 +19,12 @@
 
 fun statement_binds (name, prop) =
   let
-    val concl = Logic.strip_imp_concl prop;
-    val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
-      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
+    val concl = Logic.strip_assums_concl prop;
+    val parms = Logic.strip_params prop;
+    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
+
+    val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
+      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
   in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
 
 fun goal prop = statement_binds ("thesis", prop);