have_tthms;
authorwenzelm
Tue Nov 17 14:25:40 1998 +0100 (1998-11-17)
changeset 5919a5b2d4b9ed6f
parent 5918 4cbd726577f7
child 5920 d7e35f45b72c
have_tthms;
assume: store actual asms;
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Nov 17 14:25:02 1998 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Nov 17 14:25:40 1998 +0100
     1.3 @@ -45,8 +45,8 @@
     1.4    val put_tthm: string * tthm -> context -> context
     1.5    val put_tthms: string * tthm list -> context -> context
     1.6    val put_tthmss: (string * tthm list) list -> context -> context
     1.7 -  val have_tthms: string -> context attribute list
     1.8 -    -> (tthm * context attribute list) list -> context -> context * (string * tthm list)
     1.9 +  val have_tthmss: string -> context attribute list
    1.10 +    -> (tthm list * context attribute list) list -> context -> context * (string * tthm list)
    1.11    val assumptions: context -> tthm list
    1.12    val fixed_names: context -> string list
    1.13    val assume: string -> context attribute list -> string list -> context
    1.14 @@ -556,15 +556,15 @@
    1.15    | put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths;
    1.16  
    1.17  
    1.18 -(* have_tthms *)
    1.19 +(* have_tthmss *)
    1.20  
    1.21 -fun have_tthms name more_attrs ths_attrs ctxt =
    1.22 +fun have_tthmss name more_attrs ths_attrs ctxt =
    1.23    let
    1.24      fun app ((ct, ths), (th, attrs)) =
    1.25 -      let val (ct', th') = Attribute.apply ((ct, th), attrs @ more_attrs)
    1.26 +      let val (ct', th') = Attribute.applys ((ct, th), attrs @ more_attrs)
    1.27        in (ct', th' :: ths) end
    1.28      val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
    1.29 -    val thms = rev rev_thms;
    1.30 +    val thms = flat (rev rev_thms);
    1.31    in (ctxt' |> put_tthms (name, thms), (name, thms)) end;
    1.32  
    1.33  
    1.34 @@ -583,16 +583,18 @@
    1.35    let
    1.36      val (ctxt', props) = foldl_map prep (ctxt, raw_props);
    1.37      val sign = sign_of ctxt';
    1.38 -    val ths = map (fn t => ((Thm.assume (Thm.cterm_of sign t), []), [])) props;
    1.39  
    1.40 +    val asms = map (Attribute.tthm_of o Thm.assume o Thm.cterm_of sign) props;
    1.41 +
    1.42 +    val ths = map (fn th => ([th], [])) asms;
    1.43      val (ctxt'', (_, tthms)) =
    1.44        ctxt'
    1.45 -      |> have_tthms name (Attribute.tag_assumption :: attrs) ths
    1.46 +      |> have_tthmss name (attrs @ [Attribute.tag_assumption]) ths
    1.47  
    1.48      val ctxt''' =
    1.49        ctxt''
    1.50        |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
    1.51 -        (thy, data, (assumes @ [(name, tthms)], fixes), binds, thms, defs));
    1.52 +        (thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs));
    1.53    in (ctxt''', (name, tthms)) end;
    1.54  
    1.55  val assume = gen_assume (prep_declare read_prop);