admit unbinding;
authorwenzelm
Sat Sep 25 13:07:48 1999 +0200 (1999-09-25)
changeset 759940b7f7f51208
parent 7598 af320257c902
child 7600 73f91da46230
admit unbinding;
src/Pure/Isar/auto_bind.ML
     1.1 --- a/src/Pure/Isar/auto_bind.ML	Sat Sep 25 13:06:59 1999 +0200
     1.2 +++ b/src/Pure/Isar/auto_bind.ML	Sat Sep 25 13:07:48 1999 +0200
     1.3 @@ -7,8 +7,8 @@
     1.4  
     1.5  signature AUTO_BIND =
     1.6  sig
     1.7 -  val goal: term -> (indexname * term) list
     1.8 -  val facts: string -> term list -> (indexname * term) list
     1.9 +  val goal: term -> (indexname * term option) list
    1.10 +  val facts: string -> term list -> (indexname * term option) list
    1.11  end;
    1.12  
    1.13  structure AutoBind: AUTO_BIND =
    1.14 @@ -23,8 +23,8 @@
    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", prop), (name ^ "_concl", list_abs concl)] @
    1.19 -      (case concl of Const ("Trueprop", _) $ t => [(name, list_abs t)] | _ => []);
    1.20 +    val env = [(name ^ "_prop", Some prop), (name ^ "_concl", Some (list_abs concl)),
    1.21 +      (name, case concl of Const ("Trueprop", _) $ t => Some (list_abs t) | _ => None)];
    1.22    in map (fn (s, t) => ((s, 0), t)) env end;
    1.23  
    1.24  fun goal prop = statement_binds ("thesis", prop);
    1.25 @@ -33,9 +33,8 @@
    1.26  (* facts *)
    1.27  
    1.28  fun dddot_bind prop =
    1.29 -  (case Logic.strip_imp_concl prop of
    1.30 -    Const ("Trueprop", _) $ (_ $ t) => [(Syntax.dddot_indexname, t)]
    1.31 -  | _ => []);
    1.32 +  [(Syntax.dddot_indexname,
    1.33 +      case Logic.strip_imp_concl prop of Const ("Trueprop", _) $ (_ $ t) => Some t | _ => None)];
    1.34  
    1.35  fun facts _ [] = []
    1.36    | facts name props =