src/Pure/Isar/auto_bind.ML
changeset 7331 aee8f76fe54c
parent 7048 3535eec33c50
child 7452 c2289eabf706
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Tue Aug 24 11:43:30 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Tue Aug 24 11:50:17 1999 +0200
     1.3 @@ -19,9 +19,12 @@
     1.4  
     1.5  fun statement_binds (name, prop) =
     1.6    let
     1.7 -    val concl = Logic.strip_imp_concl prop;
     1.8 -    val env = [(name ^ "_prop", prop), (name ^ "_concl", concl)] @
     1.9 -      (case concl of Const ("Trueprop", _) $ t => [(name, t)] | _ => []);
    1.10 +    val concl = Logic.strip_assums_concl prop;
    1.11 +    val parms = Logic.strip_params prop;
    1.12 +    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    1.13 +
    1.14 +    val env = [(name ^ "_prop", prop), (name ^ "_concl", list_abs concl)] @
    1.15 +      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
    1.16    in map (fn (s, t) => ((Syntax.binding s, 0), t)) env end;
    1.17  
    1.18  fun goal prop = statement_binds ("thesis", prop);