src/Pure/Isar/element.ML
changeset 19585 70a1ce3b23ae
parent 19482 9f11af8f7ef9
child 19731 581cdbdbba9a
     1.1 --- a/src/Pure/Isar/element.ML	Sun May 07 00:21:13 2006 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Sun May 07 00:22:05 2006 +0200
     1.3 @@ -8,14 +8,14 @@
     1.4  signature ELEMENT =
     1.5  sig
     1.6    datatype ('typ, 'term) stmt =
     1.7 -    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
     1.8 +    Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
     1.9      Obtains of (string * ((string * 'typ option) list * 'term list)) list
    1.10    type statement  (*= (string, string) stmt*)
    1.11    type statement_i  (*= (typ, term) stmt*)
    1.12    datatype ('typ, 'term, 'fact) ctxt =
    1.13      Fixes of (string * 'typ option * mixfix) list |
    1.14      Constrains of (string * 'typ) list |
    1.15 -    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.16 +    Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
    1.17      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.18      Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
    1.19    type context (*= (string, string, thmref) ctxt*)
    1.20 @@ -49,7 +49,7 @@
    1.21  (** conclusions **)
    1.22  
    1.23  datatype ('typ, 'term) stmt =
    1.24 -  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.25 +  Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
    1.26    Obtains of (string * ((string * 'typ option) list * 'term list)) list;
    1.27  
    1.28  type statement = (string, string) stmt;
    1.29 @@ -64,7 +64,7 @@
    1.30  datatype ('typ, 'term, 'fact) ctxt =
    1.31    Fixes of (string * 'typ option * mixfix) list |
    1.32    Constrains of (string * 'typ) list |
    1.33 -  Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    1.34 +  Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
    1.35    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    1.36    Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
    1.37  
    1.38 @@ -76,8 +76,7 @@
    1.39         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    1.40     | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    1.41     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    1.42 -      ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
    1.43 -        (term t, (map term ps, map term qs))))))
    1.44 +      ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
    1.45     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    1.46        ((name a, map attrib atts), (term t, map term ps))))
    1.47     | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
    1.48 @@ -255,10 +254,11 @@
    1.49  
    1.50      fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
    1.51        | prt_var (x, NONE) = Pretty.str x;
    1.52 +    val prt_vars =  separate (Pretty.keyword "and") o map prt_var;
    1.53  
    1.54      fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
    1.55        | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
    1.56 -          (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
    1.57 +          (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
    1.58    in
    1.59      fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
    1.60       | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
    1.61 @@ -349,9 +349,9 @@
    1.62      val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
    1.63    in
    1.64      pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
    1.65 -    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
    1.66 +    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
    1.67      pretty_stmt ctxt
    1.68 -     (if null cases then Shows [(("", []), [(concl, ([], []))])]
    1.69 +     (if null cases then Shows [(("", []), [(concl, [])])]
    1.70        else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
    1.71    end |> thm_name kind raw_th;
    1.72