src/Pure/Isar/auto_bind.ML
changeset 8612 e8ef58d6d6eb
parent 8227 d67db92897df
child 8807 0046be1769f9
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Thu Mar 30 14:20:42 2000 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Thu Mar 30 14:21:28 2000 +0200
     1.3 @@ -26,16 +26,18 @@
     1.4  
     1.5  (** bindings **)
     1.6  
     1.7 +fun list_abs parms tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
     1.8 +
     1.9 +
    1.10  (* goal *)
    1.11  
    1.12  fun statement_binds (name, prop) =
    1.13    let
    1.14      val concl = Logic.strip_assums_concl prop;
    1.15      val parms = Logic.strip_params prop;
    1.16 -    fun list_abs tm = foldr (fn ((x, T), t) => Abs (x, T, t)) (parms, tm);
    1.17  
    1.18 -    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
    1.19 -      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    1.20 +    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs parms concl)),
    1.21 +      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs parms t) | _ => None)];
    1.22    in map (fn (s, t) => ((s, 0), t)) env end;
    1.23  
    1.24  fun goal prop = statement_binds (thesisN, prop);
    1.25 @@ -43,14 +45,15 @@
    1.26  
    1.27  (* facts *)
    1.28  
    1.29 -fun dddot_bind prop =
    1.30 -  [(Syntax.dddot_indexname,
    1.31 -      case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
    1.32 +fun get_subject prop =
    1.33 +  (case (Logic.strip_assums_concl prop) of
    1.34 +    Const ("Trueprop", _) $ (_ $ t) => Some (list_abs (Logic.strip_params prop) t)
    1.35 +  | _ => None);
    1.36  
    1.37  fun facts _ [] = []
    1.38    | facts name props =
    1.39        let val prop = Library.last_elem props
    1.40 -      in dddot_bind prop @ statement_binds (thisN, prop) end;
    1.41 +      in [(Syntax.dddot_indexname, get_subject prop)] @ statement_binds (thisN, prop) end;
    1.42  
    1.43  
    1.44  (* atomic_thesis *)