# HG changeset patch
# User wenzelm
# Date 1146954125 -7200
# Node ID 70a1ce3b23aeeda0c248e1313e662b2effb5c50c
# Parent  606d6a73e6d980f9cc2355d8de5f983d22311915
removed 'concl is' patterns;

diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOL/List.thy
--- a/src/HOL/List.thy	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/List.thy	Sun May 07 00:22:05 2006 +0200
@@ -818,7 +818,7 @@
 lemma Cons_eq_filterD:
  "x#xs = filter P ys \<Longrightarrow>
   \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
-  (concl is "\<exists>us vs. ?P ys us vs")
+  (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
 proof(induct ys)
   case Nil thus ?case by simp
 next
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOL/Tools/function_package/fundef_package.ML
--- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -68,7 +68,7 @@
     in
 	thy |> ProofContext.init
 	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
-	    (map (fn t => (("", []), [(t, ([], []))])) props)
+	    (map (fn t => (("", []), [(t, [])])) props)
     end
 
 
@@ -138,7 +138,7 @@
 	    |> ProofContext.note_thmss_i [(("termination_intro", 
 					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
 	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
-	    [(("", []), [(goal, ([], []))])]
+	    [(("", []), [(goal, [])])]
     end	
   | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
     let
@@ -148,7 +148,7 @@
     in
 	thy |> ProofContext.init
 	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
-	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
+	    [(("", []), [(subs, []), (dcl, [])])]
     end	
 
 
@@ -192,4 +192,4 @@
 end;
 
 
-end
\ No newline at end of file
+end
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/recdef_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -284,7 +284,7 @@
     val tc = List.nth (tcs, i - 1) handle Subscript =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
-  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, []) thy end;
 
 val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/specification_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -231,7 +231,7 @@
     in
       IsarThy.theorem_i PureThy.internalK
         ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
-        (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
+        (HOLogic.mk_Trueprop ex_prop, []) thy
     end
 
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -271,7 +271,7 @@
     fun att (thy, th) =
       let val ((th', _), thy') = att_result th thy
       in (thy', th') end;
-  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) thy end;
 
 in
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/HOLCF/pcpodef_package.ML
--- a/src/HOLCF/pcpodef_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/HOLCF/pcpodef_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -177,7 +177,7 @@
   let
     val (goal, att) =
       gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
-  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end;
+  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, []) thy end;
 
 fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
 fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/element.ML	Sun May 07 00:22:05 2006 +0200
@@ -8,14 +8,14 @@
 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*)
@@ -49,7 +49,7 @@
 (** 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;
@@ -64,7 +64,7 @@
 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;
 
@@ -76,8 +76,7 @@
        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) =>
@@ -255,10 +254,11 @@
 
     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)
@@ -349,9 +349,9 @@
     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;
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/isar_thy.ML	Sun May 07 00:22:05 2006 +0200
@@ -24,18 +24,16 @@
     theory -> Proof.context * theory
   val declare_theorems: xstring option ->
     (thmref * Attrib.src list) list -> theory -> Proof.context * theory
-  val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+  val have: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
-  val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    bool -> Proof.state -> Proof.state
-  val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+  val hence: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
-  val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
+  val show: ((string * Attrib.src list) * (string * string list) list) list ->
     bool -> Proof.state -> Proof.state
-  val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
-    theory -> Proof.state
-  val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
-    theory -> Proof.state
+  val thus: ((string * Attrib.src list) * (string * string list) list) list ->
+    bool -> Proof.state -> Proof.state
+  val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state
+  val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state
   val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: Method.text * Method.text option ->
     Toplevel.transition -> Toplevel.transition
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun May 07 00:22:05 2006 +0200
@@ -84,7 +84,7 @@
   in
     ctxt
     |> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
-    |> ProofContext.add_assms_i def_export [(("", []), [(eq, ([], []))])]
+    |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
     |>> (fn [(_, [th])] => (x', th))
   end;
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/locale.ML	Sun May 07 00:22:05 2006 +0200
@@ -56,13 +56,13 @@
 
   (* Processing of locale statements *)
   val read_context_statement: xstring option -> Element.context element list ->
-    (string * (string list * string list)) list list -> Proof.context ->
+    (string * string list) list list -> Proof.context ->
     string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
-      (term * (term list * term list)) list list
+      (term * term list) list list
   val cert_context_statement: string option -> Element.context_i element list ->
-    (term * (term list * term list)) list list -> Proof.context ->
+    (term * term list) list list -> Proof.context ->
     string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
-      (term * (term list * term list)) list list
+      (term * term list) list list
 
   (* Diagnostic functions *)
   val print_locales: theory -> unit
@@ -864,7 +864,7 @@
         ctxt |> ProofContext.add_assms_i LocalDefs.def_export
           (defs' |> map (fn ((name, atts), (t, ps)) =>
             let val ((c, _), t') = LocalDefs.cert_def ctxt t
-            in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
+            in ((if name = "" then Thm.def_name c else name, atts), [(t', ps)]) end))
       in ((ctxt', Assumed axs), []) end
   | activate_elem _ ((ctxt, Derived ths), Defines defs) =
       ((ctxt, Derived ths), [])
@@ -947,7 +947,7 @@
       let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
       in (ctxt', []) end
   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
-  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
+  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
 
 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
@@ -1024,7 +1024,7 @@
       let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
       in (ctxt', []) end
   | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
-  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
+  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
   | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
 
 fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
@@ -1136,7 +1136,7 @@
       in
         (case elem of
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
-            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
+            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
             (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
         | e => e)
@@ -1149,7 +1149,7 @@
   | finish_ext_elem _ close (Assumes asms, propp) =
       close (Assumes (map #1 asms ~~ propp))
   | finish_ext_elem _ close (Defines defs, propp) =
-      close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
+      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
   | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
 
 
@@ -1667,7 +1667,7 @@
             thy |> def_pred aname parms defs exts exts';
           val elemss' =
             change_elemss axioms elemss
-            @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
+            @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
         in
           def_thy
           |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
@@ -2145,7 +2145,7 @@
   in (propss, activate) end;
 
 fun prep_propp propss = propss |> map (fn ((name, _), props) =>
-  (("", []), map (rpair ([], []) o Logic.protect) props));
+  (("", []), map (rpair [] o Logic.protect) props));
 
 fun prep_result propps thmss =
   ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun May 07 00:22:05 2006 +0200
@@ -40,19 +40,18 @@
 signature OBTAIN =
 sig
   val obtain: string -> (string * string option) list ->
-    ((string * Attrib.src list) * (string * (string list * string list)) list) list
+    ((string * Attrib.src list) * (string * string list) list) list
     -> bool -> Proof.state -> Proof.state
   val obtain_i: string -> (string * typ option) list ->
-    ((string * attribute list) * (term * (term list * term list)) list) list
+    ((string * attribute list) * (term * term list) list) list
     -> bool -> Proof.state -> Proof.state
   val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
   val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
   val statement: (string * ((string * 'typ option) list * 'term list)) list ->
     (('typ, 'term, 'fact) Element.ctxt list *
-      ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) *
-    (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context ->
-      (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) *
-        Proof.context)
+      ((string * Attrib.src list) * ('term * 'term list) list) list) *
+    (((string * Attrib.src list) * (term * term list) list) list -> Proof.context ->
+      (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context)
 end;
 
 structure Obtain: OBTAIN =
@@ -151,13 +150,13 @@
   in
     state
     |> Proof.enter_forward
-    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
+    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
     |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
     |> Proof.fix_i [(thesisN, NONE)]
-    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
+    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
     |> `Proof.the_facts
     ||> Proof.chain_facts chain_facts
-    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
+    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
     |-> Proof.refine_insert
   end;
 
@@ -246,7 +245,7 @@
         val ps = map dest_Free ts;
         val asms =
           Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
-          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
+          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
         val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
       in
         Proof.fix_i (map (apsnd SOME) parms)
@@ -285,7 +284,7 @@
       cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
     val elems = cases |> map (fn (_, (vars, _)) =>
       Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
-    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
+    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props));
 
     fun mk_stmt stmt ctxt =
       let
@@ -306,14 +305,14 @@
           in
             ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
             ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
-              [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])]
+              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
             |>> (fn [(_, [th])] => th)
           end;
         val (ths, ctxt') = ctxt
           |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
           |> fold_map assume_case (cases ~~ stmt)
           |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
-      in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end;
+      in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
   in ((elems, concl), mk_stmt) end;
 
 end;
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Sun May 07 00:22:05 2006 +0200
@@ -65,7 +65,7 @@
   val simple_fixes: token list -> (string * string option) list * token list
   val term: token list -> string * token list
   val prop: token list -> string * token list
-  val propp: token list -> (string * (string list * string list)) * token list
+  val propp: token list -> (string * string list) * token list
   val termp: token list -> (string * string list) * token list
   val arguments: token list -> Args.T list * token list
   val attribs: token list -> Attrib.src list * token list
@@ -91,7 +91,7 @@
   val locale_element: token list -> Element.context Locale.element * token list
   val context_element: token list -> Element.context * token list
   val statement: token list ->
-    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list * token list
+    ((bstring * Attrib.src list) * (string * string list) list) list * token list
   val general_statement: token list ->
     (Element.context Locale.element list * Element.statement) * OuterLex.token list
   val statement_keyword: token list -> string * token list
@@ -281,11 +281,8 @@
 
 val is_terms = Scan.repeat1 ($$$ "is" |-- term);
 val is_props = Scan.repeat1 ($$$ "is" |-- prop);
-val concl_props = $$$ "concl" |-- !!! is_props;
-val any_props = concl_props >> pair [] || is_props -- Scan.optional concl_props [];
 
-val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
-val propp' = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
+val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
 val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
 
 
@@ -363,7 +360,7 @@
     >> Element.Constrains ||
   $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
     >> Element.Assumes ||
-  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
+  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp))
     >> Element.Defines ||
   $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
     >> Element.Notes;
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/proof.ML	Sun May 07 00:22:05 2006 +0200
@@ -47,23 +47,15 @@
   val fix: (string * string option) list -> state -> state
   val fix_i: (string * typ option) list -> state -> state
   val assm: ProofContext.export ->
-    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    state -> state
+    ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   val assm_i: ProofContext.export ->
-    ((string * attribute list) * (term * (term list * term list)) list) list
-    -> state -> state
-  val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    state -> state
-  val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
-    -> state -> state
-  val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
-    -> state -> state
-  val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
-    -> state -> state
-  val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
-    state -> state
-  val def_i: ((string * attribute list) * (string * (term * term list))) list ->
-    state -> state
+    ((string * attribute list) * (term * term list) list) list -> state -> state
+  val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+  val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
+  val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
+  val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
+  val def: ((string * Attrib.src list) * (string * (string * string list))) list -> state -> state
+  val def_i: ((string * attribute list) * (string * (term * term list))) list -> state -> state
   val chain: state -> state
   val chain_facts: thm list -> state -> state
   val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
@@ -114,25 +106,19 @@
   val global_done_proof: state -> context * theory
   val global_skip_proof: bool -> state -> context * theory
   val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    bool -> state -> state
+    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * attribute list) * (term * (term list * term list)) list) list ->
-    bool -> state -> state
+    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    bool -> state -> state
+    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
-    ((string * attribute list) * (term * (term list * term list)) list) list ->
-    bool -> state -> state
+    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string option -> string * Attrib.src list ->
-    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
-    context -> state
+    ((string * Attrib.src list) * (string * string list) list) list -> context -> state
   val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string option -> string * attribute list ->
-    ((string * attribute list) * (term * (term list * term list)) list) list ->
-    context -> state
+    ((string * attribute list) * (term * term list) list) list -> context -> state
 end;
 
 structure Proof: PROOF =
@@ -580,7 +566,7 @@
   in
     state'
     |> fix (map (rpair NONE) xs)
-    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
+    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs)
   end;
 
 in
@@ -681,7 +667,7 @@
     val atts = map (prep_att (theory_of state)) raw_atts;
     val (asms, state') = state |> map_context_result (fn ctxt =>
       ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
-    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
+    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
   in
     state'
     |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sun May 07 00:22:05 2006 +0200
@@ -88,21 +88,21 @@
   val auto_bind_facts: term list -> context -> context
   val match_bind: bool -> (string list * string) list -> context -> term list * context
   val match_bind_i: bool -> (term list * term) list -> context -> term list * context
-  val read_propp: context * (string * (string list * string list)) list list
-    -> context * (term * (term list * term list)) list list
-  val cert_propp: context * (term * (term list * term list)) list list
-    -> context * (term * (term list * term list)) list list
-  val read_propp_schematic: context * (string * (string list * string list)) list list
-    -> context * (term * (term list * term list)) list list
-  val cert_propp_schematic: context * (term * (term list * term list)) list list
-    -> context * (term * (term list * term list)) list list
-  val bind_propp: context * (string * (string list * string list)) list list
+  val read_propp: context * (string * string list) list list
+    -> context * (term * term list) list list
+  val cert_propp: context * (term * term list) list list
+    -> context * (term * term list) list list
+  val read_propp_schematic: context * (string * string list) list list
+    -> context * (term * term list) list list
+  val cert_propp_schematic: context * (term * term list) list list
+    -> context * (term * term list) list list
+  val bind_propp: context * (string * string list) list list
     -> context * (term list list * (context -> context))
-  val bind_propp_i: context * (term * (term list * term list)) list list
+  val bind_propp_i: context * (term * term list) list list
     -> context * (term list list * (context -> context))
-  val bind_propp_schematic: context * (string * (string list * string list)) list list
+  val bind_propp_schematic: context * (string * string list) list list
     -> context * (term list list * (context -> context))
-  val bind_propp_schematic_i: context * (term * (term list * term list)) list list
+  val bind_propp_schematic_i: context * (term * term list) list list
     -> context * (term list list * (context -> context))
   val fact_tac: thm list -> int -> tactic
   val some_fact_tac: context -> int -> tactic
@@ -142,10 +142,10 @@
   val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
   val bind_fixes: string list -> context -> (term -> term) * context
   val add_assms: export ->
-    ((string * attribute list) * (string * (string list * string list)) list) list ->
+    ((string * attribute list) * (string * string list) list) list ->
     context -> (bstring * thm list) list * context
   val add_assms_i: export ->
-    ((string * attribute list) * (term * (term list * term list)) list) list ->
+    ((string * attribute list) * (term * term list) list) list ->
     context -> (bstring * thm list) list * context
   val assume_export: export
   val presume_export: export
@@ -833,11 +833,12 @@
 
 (* simult_matches *)
 
-fun simult_matches ctxt [] = []
-  | simult_matches ctxt pairs =
+fun simult_matches _ (_, []) = []
+  | simult_matches ctxt (t, pats) =
       let
         fun fail () = error "Pattern match failed!";
 
+        val pairs = map (rpair t) pats;
         val maxidx = fold (fn (t1, t2) => fn i =>
           Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
         val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
@@ -885,8 +886,8 @@
 fun prep_bind prep_pats (raw_pats, t) ctxt =
   let
     val ctxt' = declare_term t ctxt;
-    val pats = prep_pats (fastype_of t) ctxt' raw_pats;
-    val binds = simult_matches ctxt' (map (rpair t) pats);
+    val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats;
+    val binds = simult_matches ctxt' (t, pats);
   in (binds, ctxt') end;
 
 fun gen_binds prep_terms prep_pats gen raw_binds ctxt =
@@ -919,23 +920,18 @@
 
 fun prep_propp schematic prep_props prep_pats (context, args) =
   let
-    fun prep (_, (raw_pats1, raw_pats2)) (ctxt, prop :: props) =
-          let
-            val ctxt' = declare_term prop ctxt;
-            val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2);    (*simultaneous type inference!*)
-          in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end
+    fun prep (_, raw_pats) (ctxt, prop :: props) =
+          let val ctxt' = declare_term prop ctxt
+          in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end
       | prep _ _ = sys_error "prep_propp";
     val (propp, (context', _)) = (fold_map o fold_map) prep args
       (context, prep_props schematic context (maps (map fst) args));
   in (context', propp) end;
 
-fun matches ctxt (prop, (pats1, pats2)) =
-  simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2);
-
 fun gen_bind_propp prepp (ctxt, raw_args) =
   let
     val (ctxt', args) = prepp (ctxt, raw_args);
-    val binds = flat (flat (map (map (matches ctxt')) args));
+    val binds = flat (flat (map (map (simult_matches ctxt')) args));
     val propss = map (map #1) args;
 
     (*generalize result: context evaluated now, binds added later*)
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Isar/specification.ML	Sun May 07 00:22:05 2006 +0200
@@ -46,7 +46,7 @@
     val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
     val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
     val ((specs, vs), specs_ctxt) =
-      prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
+      prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs)
       |> swap |>> map (map fst)
       ||>> fold_map ProofContext.inferred_param xs;
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Sun May 07 00:22:05 2006 +0200
@@ -301,7 +301,7 @@
   thy
   |> ProofContext.init
   |> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
-       (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
+       (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
 
 in
 
diff -r 606d6a73e6d9 -r 70a1ce3b23ae src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sun May 07 00:21:13 2006 +0200
+++ b/src/Pure/axclass.ML	Sun May 07 00:22:05 2006 +0200
@@ -283,7 +283,7 @@
       |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
       |> Logic.close_form;
 
-    val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs)
+    val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
       |> snd |> map (map (prep_axiom o fst));
     val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;