src/Pure/Isar/element.ML

 *)
 
 signature ELEMENT =
 sig
   datatype ('typ, 'term) stmt =
-    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+    Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
     Obtains of (string * ((string * 'typ option) list * 'term list)) list
   type statement  (*= (string, string) stmt*)
   type statement_i  (*= (typ, term) stmt*)
   datatype ('typ, 'term, 'fact) ctxt =
     Fixes of (string * 'typ option * mixfix) list |
     Constrains of (string * 'typ) list |
-    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+    Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
     Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
     Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
   type context (*= (string, string, thmref) ctxt*)
   type context_i (*= (typ, term, thm list) ctxt*)
   val map_ctxt: {name: string -> string,

 
 
 (** conclusions **)
 
 datatype ('typ, 'term) stmt =
-  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+  Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
   Obtains of (string * ((string * 'typ option) list * 'term list)) list;
 
 type statement = (string, string) stmt;
 type statement_i = (typ, term) stmt;
 

 (* datatype ctxt *)
 
 datatype ('typ, 'term, 'fact) ctxt =
   Fixes of (string * 'typ option * mixfix) list |
   Constrains of (string * 'typ) list |
-  Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
+  Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
   Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
   Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
 
 type context = (string, string, thmref) ctxt;
 type context_i = (typ, term, thm list) ctxt;

 fun map_ctxt {name, var, typ, term, fact, attrib} =
   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) =>
        let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
-      ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
-        (term t, (map term ps, map term qs))))))
+      ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
       ((name a, map attrib atts), (term t, map term ps))))
    | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
       ((name a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
 

     fun prt_show (a, ts) =
       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
 
     fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
       | prt_var (x, NONE) = Pretty.str x;
+    val prt_vars =  separate (Pretty.keyword "and") o map prt_var;
 
     fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
       | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
-          (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
+          (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
   in
     fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
      | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
   end;
 

     val (prems, concl) = Logic.strip_horn prop;
     val thesis = ObjectLogic.fixed_judgment thy AutoBind.thesisN;
     val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
   in
     pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
-    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
+    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
     pretty_stmt ctxt
-     (if null cases then Shows [(("", []), [(concl, ([], []))])]
+     (if null cases then Shows [(("", []), [(concl, [])])]
       else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
   end |> thm_name kind raw_th;
 
 end;