removed 'concl is' patterns;
authorwenzelm
Sun May 07 00:22:05 2006 +0200 (2006-05-07)
changeset 1958570a1ce3b23ae
parent 19584 606d6a73e6d9
child 19586 a14871b57387
removed 'concl is' patterns;
src/HOL/List.thy
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/specification_package.ML
src/HOL/Tools/typedef_package.ML
src/HOLCF/pcpodef_package.ML
src/Pure/Isar/element.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Tools/class_package.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/List.thy	Sun May 07 00:21:13 2006 +0200
     1.2 +++ b/src/HOL/List.thy	Sun May 07 00:22:05 2006 +0200
     1.3 @@ -818,7 +818,7 @@
     1.4  lemma Cons_eq_filterD:
     1.5   "x#xs = filter P ys \<Longrightarrow>
     1.6    \<exists>us vs. ys = us @ x # vs \<and> (\<forall>u\<in>set us. \<not> P u) \<and> P x \<and> xs = filter P vs"
     1.7 -  (concl is "\<exists>us vs. ?P ys us vs")
     1.8 +  (is "_ \<Longrightarrow> \<exists>us vs. ?P ys us vs")
     1.9  proof(induct ys)
    1.10    case Nil thus ?case by simp
    1.11  next
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:21:13 2006 +0200
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Sun May 07 00:22:05 2006 +0200
     2.3 @@ -68,7 +68,7 @@
     2.4      in
     2.5  	thy |> ProofContext.init
     2.6  	    |> Proof.theorem_i PureThy.internalK NONE (fundef_afterqed congs curry_info name data natts) NONE ("", [])
     2.7 -	    (map (fn t => (("", []), [(t, ([], []))])) props)
     2.8 +	    (map (fn t => (("", []), [(t, [])])) props)
     2.9      end
    2.10  
    2.11  
    2.12 @@ -138,7 +138,7 @@
    2.13  	    |> ProofContext.note_thmss_i [(("termination_intro", 
    2.14  					    [ContextRules.intro_query NONE]), [([total_intro], [])])] |> snd
    2.15  	    |> Proof.theorem_i PureThy.internalK NONE (total_termination_afterqed name) NONE ("", [])
    2.16 -	    [(("", []), [(goal, ([], []))])]
    2.17 +	    [(("", []), [(goal, [])])]
    2.18      end	
    2.19    | fundef_setup_termination_proof name (SOME (dom_name, dom)) thy =
    2.20      let
    2.21 @@ -148,7 +148,7 @@
    2.22      in
    2.23  	thy |> ProofContext.init
    2.24  	    |> Proof.theorem_i PureThy.internalK NONE (K I) NONE ("", [])
    2.25 -	    [(("", []), [(subs, ([], [])), (dcl, ([], []))])]
    2.26 +	    [(("", []), [(subs, []), (dcl, [])])]
    2.27      end	
    2.28  
    2.29  
    2.30 @@ -192,4 +192,4 @@
    2.31  end;
    2.32  
    2.33  
    2.34 -end
    2.35 \ No newline at end of file
    2.36 +end
     3.1 --- a/src/HOL/Tools/recdef_package.ML	Sun May 07 00:21:13 2006 +0200
     3.2 +++ b/src/HOL/Tools/recdef_package.ML	Sun May 07 00:22:05 2006 +0200
     3.3 @@ -284,7 +284,7 @@
     3.4      val tc = List.nth (tcs, i - 1) handle Subscript =>
     3.5        error ("No termination condition #" ^ string_of_int i ^
     3.6          " in recdef definition of " ^ quote name);
     3.7 -  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, ([], [])) thy end;
     3.8 +  in IsarThy.theorem_i PureThy.internalK (bname, atts) (HOLogic.mk_Trueprop tc, []) thy end;
     3.9  
    3.10  val recdef_tc = gen_recdef_tc Attrib.attribute Sign.intern_const;
    3.11  val recdef_tc_i = gen_recdef_tc (K I) (K I);
     4.1 --- a/src/HOL/Tools/specification_package.ML	Sun May 07 00:21:13 2006 +0200
     4.2 +++ b/src/HOL/Tools/specification_package.ML	Sun May 07 00:22:05 2006 +0200
     4.3 @@ -231,7 +231,7 @@
     4.4      in
     4.5        IsarThy.theorem_i PureThy.internalK
     4.6          ("", [add_spec axiomatic (zip3 names cnames overloaded), post_proc])
     4.7 -        (HOLogic.mk_Trueprop ex_prop, ([], [])) thy
     4.8 +        (HOLogic.mk_Trueprop ex_prop, []) thy
     4.9      end
    4.10  
    4.11  
     5.1 --- a/src/HOL/Tools/typedef_package.ML	Sun May 07 00:21:13 2006 +0200
     5.2 +++ b/src/HOL/Tools/typedef_package.ML	Sun May 07 00:22:05 2006 +0200
     5.3 @@ -271,7 +271,7 @@
     5.4      fun att (thy, th) =
     5.5        let val ((th', _), thy') = att_result th thy
     5.6        in (thy', th') end;
     5.7 -  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([goal_pat], [])) thy end;
     5.8 +  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, [goal_pat]) thy end;
     5.9  
    5.10  in
    5.11  
     6.1 --- a/src/HOLCF/pcpodef_package.ML	Sun May 07 00:21:13 2006 +0200
     6.2 +++ b/src/HOLCF/pcpodef_package.ML	Sun May 07 00:22:05 2006 +0200
     6.3 @@ -177,7 +177,7 @@
     6.4    let
     6.5      val (goal, att) =
     6.6        gen_prepare_pcpodef prep_term pcpo def name typ set opt_morphs thy;
     6.7 -  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, ([], [])) thy end;
     6.8 +  in IsarThy.theorem_i PureThy.internalK ("", [att]) (goal, []) thy end;
     6.9  
    6.10  fun pcpodef_proof x = gen_pcpodef_proof read_term true x;
    6.11  fun pcpodef_proof_i x = gen_pcpodef_proof cert_term true x;
     7.1 --- a/src/Pure/Isar/element.ML	Sun May 07 00:21:13 2006 +0200
     7.2 +++ b/src/Pure/Isar/element.ML	Sun May 07 00:22:05 2006 +0200
     7.3 @@ -8,14 +8,14 @@
     7.4  signature ELEMENT =
     7.5  sig
     7.6    datatype ('typ, 'term) stmt =
     7.7 -    Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
     7.8 +    Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
     7.9      Obtains of (string * ((string * 'typ option) list * 'term list)) list
    7.10    type statement  (*= (string, string) stmt*)
    7.11    type statement_i  (*= (typ, term) stmt*)
    7.12    datatype ('typ, 'term, 'fact) ctxt =
    7.13      Fixes of (string * 'typ option * mixfix) list |
    7.14      Constrains of (string * 'typ) list |
    7.15 -    Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    7.16 +    Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
    7.17      Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    7.18      Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list
    7.19    type context (*= (string, string, thmref) ctxt*)
    7.20 @@ -49,7 +49,7 @@
    7.21  (** conclusions **)
    7.22  
    7.23  datatype ('typ, 'term) stmt =
    7.24 -  Shows of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    7.25 +  Shows of ((string * Attrib.src list) * ('term * 'term list) list) list |
    7.26    Obtains of (string * ((string * 'typ option) list * 'term list)) list;
    7.27  
    7.28  type statement = (string, string) stmt;
    7.29 @@ -64,7 +64,7 @@
    7.30  datatype ('typ, 'term, 'fact) ctxt =
    7.31    Fixes of (string * 'typ option * mixfix) list |
    7.32    Constrains of (string * 'typ) list |
    7.33 -  Assumes of ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list |
    7.34 +  Assumes of ((string * Attrib.src list) * ('term * 'term list) list) list |
    7.35    Defines of ((string * Attrib.src list) * ('term * 'term list)) list |
    7.36    Notes of ((string * Attrib.src list) * ('fact * Attrib.src list) list) list;
    7.37  
    7.38 @@ -76,8 +76,7 @@
    7.39         let val (x', mx') = var (x, mx) in (x', Option.map typ T, mx') end))
    7.40     | Constrains xs => Constrains (xs |> map (fn (x, T) => (#1 (var (x, NoSyn)), typ T)))
    7.41     | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    7.42 -      ((name a, map attrib atts), propps |> map (fn (t, (ps, qs)) =>
    7.43 -        (term t, (map term ps, map term qs))))))
    7.44 +      ((name a, map attrib atts), propps |> map (fn (t, ps) => (term t, map term ps)))))
    7.45     | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    7.46        ((name a, map attrib atts), (term t, map term ps))))
    7.47     | Notes facts => Notes (facts |> map (fn ((a, atts), bs) =>
    7.48 @@ -255,10 +254,11 @@
    7.49  
    7.50      fun prt_var (x, SOME T) = Pretty.block [Pretty.str (x ^ " ::"), Pretty.brk 1, prt_typ T]
    7.51        | prt_var (x, NONE) = Pretty.str x;
    7.52 +    val prt_vars =  separate (Pretty.keyword "and") o map prt_var;
    7.53  
    7.54      fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
    7.55        | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
    7.56 -          (map prt_var xs @ [Pretty.keyword "where"] @ prt_terms ts));
    7.57 +          (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
    7.58    in
    7.59      fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
    7.60       | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
    7.61 @@ -349,9 +349,9 @@
    7.62      val (asms, cases) = take_suffix (fn prem => thesis aconv Logic.strip_assums_concl prem) prems;
    7.63    in
    7.64      pretty_ctxt ctxt (Fixes (map (fn (x, T) => (x, SOME T, NoSyn)) fixes)) @
    7.65 -    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, ([], []))])) asms)) @
    7.66 +    pretty_ctxt ctxt (Assumes (map (fn t => (("", []), [(t, [])])) asms)) @
    7.67      pretty_stmt ctxt
    7.68 -     (if null cases then Shows [(("", []), [(concl, ([], []))])]
    7.69 +     (if null cases then Shows [(("", []), [(concl, [])])]
    7.70        else Obtains (#1 (fold_map obtain cases (ctxt |> ProofContext.declare_term prop))))
    7.71    end |> thm_name kind raw_th;
    7.72  
     8.1 --- a/src/Pure/Isar/isar_thy.ML	Sun May 07 00:21:13 2006 +0200
     8.2 +++ b/src/Pure/Isar/isar_thy.ML	Sun May 07 00:22:05 2006 +0200
     8.3 @@ -24,18 +24,16 @@
     8.4      theory -> Proof.context * theory
     8.5    val declare_theorems: xstring option ->
     8.6      (thmref * Attrib.src list) list -> theory -> Proof.context * theory
     8.7 -  val have: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
     8.8 +  val have: ((string * Attrib.src list) * (string * string list) list) list ->
     8.9      bool -> Proof.state -> Proof.state
    8.10 -  val hence: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    8.11 -    bool -> Proof.state -> Proof.state
    8.12 -  val show: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    8.13 +  val hence: ((string * Attrib.src list) * (string * string list) list) list ->
    8.14      bool -> Proof.state -> Proof.state
    8.15 -  val thus: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    8.16 +  val show: ((string * Attrib.src list) * (string * string list) list) list ->
    8.17      bool -> Proof.state -> Proof.state
    8.18 -  val theorem: string -> string * Attrib.src list -> string * (string list * string list) ->
    8.19 -    theory -> Proof.state
    8.20 -  val theorem_i: string -> string * attribute list -> term * (term list * term list) ->
    8.21 -    theory -> Proof.state
    8.22 +  val thus: ((string * Attrib.src list) * (string * string list) list) list ->
    8.23 +    bool -> Proof.state -> Proof.state
    8.24 +  val theorem: string -> string * Attrib.src list -> string * string list -> theory -> Proof.state
    8.25 +  val theorem_i: string -> string * attribute list -> term * term list -> theory -> Proof.state
    8.26    val qed: Method.text option -> Toplevel.transition -> Toplevel.transition
    8.27    val terminal_proof: Method.text * Method.text option ->
    8.28      Toplevel.transition -> Toplevel.transition
     9.1 --- a/src/Pure/Isar/local_defs.ML	Sun May 07 00:21:13 2006 +0200
     9.2 +++ b/src/Pure/Isar/local_defs.ML	Sun May 07 00:22:05 2006 +0200
     9.3 @@ -84,7 +84,7 @@
     9.4    in
     9.5      ctxt
     9.6      |> ProofContext.add_fixes_i [(x, NONE, NoSyn)] |> snd
     9.7 -    |> ProofContext.add_assms_i def_export [(("", []), [(eq, ([], []))])]
     9.8 +    |> ProofContext.add_assms_i def_export [(("", []), [(eq, [])])]
     9.9      |>> (fn [(_, [th])] => (x', th))
    9.10    end;
    9.11  
    10.1 --- a/src/Pure/Isar/locale.ML	Sun May 07 00:21:13 2006 +0200
    10.2 +++ b/src/Pure/Isar/locale.ML	Sun May 07 00:22:05 2006 +0200
    10.3 @@ -56,13 +56,13 @@
    10.4  
    10.5    (* Processing of locale statements *)
    10.6    val read_context_statement: xstring option -> Element.context element list ->
    10.7 -    (string * (string list * string list)) list list -> Proof.context ->
    10.8 +    (string * string list) list list -> Proof.context ->
    10.9      string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
   10.10 -      (term * (term list * term list)) list list
   10.11 +      (term * term list) list list
   10.12    val cert_context_statement: string option -> Element.context_i element list ->
   10.13 -    (term * (term list * term list)) list list -> Proof.context ->
   10.14 +    (term * term list) list list -> Proof.context ->
   10.15      string option * (cterm list * Proof.context) * (cterm list * Proof.context) *
   10.16 -      (term * (term list * term list)) list list
   10.17 +      (term * term list) list list
   10.18  
   10.19    (* Diagnostic functions *)
   10.20    val print_locales: theory -> unit
   10.21 @@ -864,7 +864,7 @@
   10.22          ctxt |> ProofContext.add_assms_i LocalDefs.def_export
   10.23            (defs' |> map (fn ((name, atts), (t, ps)) =>
   10.24              let val ((c, _), t') = LocalDefs.cert_def ctxt t
   10.25 -            in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end))
   10.26 +            in ((if name = "" then Thm.def_name c else name, atts), [(t', ps)]) end))
   10.27        in ((ctxt', Assumed axs), []) end
   10.28    | activate_elem _ ((ctxt, Derived ths), Defines defs) =
   10.29        ((ctxt, Derived ths), [])
   10.30 @@ -947,7 +947,7 @@
   10.31        let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
   10.32        in (ctxt', []) end
   10.33    | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   10.34 -  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   10.35 +  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
   10.36    | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
   10.37  
   10.38  fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
   10.39 @@ -1024,7 +1024,7 @@
   10.40        let val (_, ctxt') = prep_vars (map (fn (x, T) => (x, SOME T, NoSyn)) csts) ctxt
   10.41        in (ctxt', []) end
   10.42    | declare_ext_elem _ (ctxt, Assumes asms) = (ctxt, map #2 asms)
   10.43 -  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, (ps, []))]) defs)
   10.44 +  | declare_ext_elem _ (ctxt, Defines defs) = (ctxt, map (fn (_, (t, ps)) => [(t, ps)]) defs)
   10.45    | declare_ext_elem _ (ctxt, Notes facts) = (ctxt, []);
   10.46  
   10.47  fun declare_elems prep_vars (ctxt, (((name, ps), Assumed _), elems)) =
   10.48 @@ -1136,7 +1136,7 @@
   10.49        in
   10.50          (case elem of
   10.51            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
   10.52 -            (a, map (fn (t, (ps, qs)) => (close_frees t, (no_binds ps, no_binds qs))) propps)))
   10.53 +            (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
   10.54          | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
   10.55              (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
   10.56          | e => e)
   10.57 @@ -1149,7 +1149,7 @@
   10.58    | finish_ext_elem _ close (Assumes asms, propp) =
   10.59        close (Assumes (map #1 asms ~~ propp))
   10.60    | finish_ext_elem _ close (Defines defs, propp) =
   10.61 -      close (Defines (map #1 defs ~~ map (fn [(t, (ps, []))] => (t, ps)) propp))
   10.62 +      close (Defines (map #1 defs ~~ map (fn [(t, ps)] => (t, ps)) propp))
   10.63    | finish_ext_elem _ _ (Notes facts, _) = Notes facts;
   10.64  
   10.65  
   10.66 @@ -1667,7 +1667,7 @@
   10.67              thy |> def_pred aname parms defs exts exts';
   10.68            val elemss' =
   10.69              change_elemss axioms elemss
   10.70 -            @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, ([], []))])]])];
   10.71 +            @ [(("", []), [Assumes [((bname ^ "_" ^ axiomsN, []), [(statement, [])])]])];
   10.72          in
   10.73            def_thy
   10.74            |> PureThy.note_thmss_qualified "" aname [((introN, []), [([intro], [])])]
   10.75 @@ -2145,7 +2145,7 @@
   10.76    in (propss, activate) end;
   10.77  
   10.78  fun prep_propp propss = propss |> map (fn ((name, _), props) =>
   10.79 -  (("", []), map (rpair ([], []) o Logic.protect) props));
   10.80 +  (("", []), map (rpair [] o Logic.protect) props));
   10.81  
   10.82  fun prep_result propps thmss =
   10.83    ListPair.map (fn ((_, props), thms) => (props ~~ thms)) (propps, thmss);
    11.1 --- a/src/Pure/Isar/obtain.ML	Sun May 07 00:21:13 2006 +0200
    11.2 +++ b/src/Pure/Isar/obtain.ML	Sun May 07 00:22:05 2006 +0200
    11.3 @@ -40,19 +40,18 @@
    11.4  signature OBTAIN =
    11.5  sig
    11.6    val obtain: string -> (string * string option) list ->
    11.7 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list
    11.8 +    ((string * Attrib.src list) * (string * string list) list) list
    11.9      -> bool -> Proof.state -> Proof.state
   11.10    val obtain_i: string -> (string * typ option) list ->
   11.11 -    ((string * attribute list) * (term * (term list * term list)) list) list
   11.12 +    ((string * attribute list) * (term * term list) list) list
   11.13      -> bool -> Proof.state -> Proof.state
   11.14    val guess: (string * string option) list -> bool -> Proof.state -> Proof.state
   11.15    val guess_i: (string * typ option) list -> bool -> Proof.state -> Proof.state
   11.16    val statement: (string * ((string * 'typ option) list * 'term list)) list ->
   11.17      (('typ, 'term, 'fact) Element.ctxt list *
   11.18 -      ((string * Attrib.src list) * ('term * ('term list * 'term list)) list) list) *
   11.19 -    (((string * Attrib.src list) * (term * (term list * term list)) list) list -> Proof.context ->
   11.20 -      (((string * Attrib.src list) * (term * (term list * term list)) list) list * thm list) *
   11.21 -        Proof.context)
   11.22 +      ((string * Attrib.src list) * ('term * 'term list) list) list) *
   11.23 +    (((string * Attrib.src list) * (term * term list) list) list -> Proof.context ->
   11.24 +      (((string * Attrib.src list) * (term * term list) list) list * thm list) * Proof.context)
   11.25  end;
   11.26  
   11.27  structure Obtain: OBTAIN =
   11.28 @@ -151,13 +150,13 @@
   11.29    in
   11.30      state
   11.31      |> Proof.enter_forward
   11.32 -    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int
   11.33 +    |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, [])])] int
   11.34      |> Proof.proof (SOME Method.succeed_text) |> Seq.hd
   11.35      |> Proof.fix_i [(thesisN, NONE)]
   11.36 -    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, ([], []))])]
   11.37 +    |> Proof.assume_i [((that_name, [ContextRules.intro_query NONE]), [(that_prop, [])])]
   11.38      |> `Proof.the_facts
   11.39      ||> Proof.chain_facts chain_facts
   11.40 -    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false
   11.41 +    ||> Proof.show_i NONE after_qed [(("", []), [(thesis, [])])] false
   11.42      |-> Proof.refine_insert
   11.43    end;
   11.44  
   11.45 @@ -246,7 +245,7 @@
   11.46          val ps = map dest_Free ts;
   11.47          val asms =
   11.48            Logic.strip_assums_hyp (Logic.nth_prem (1, Thm.prop_of rule))
   11.49 -          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), ([], [])));
   11.50 +          |> map (fn asm => (Term.betapplys (Term.list_abs (ps, asm), ts), []));
   11.51          val _ = conditional (null asms) (fn () => error "Trivial result -- nothing guessed");
   11.52        in
   11.53          Proof.fix_i (map (apsnd SOME) parms)
   11.54 @@ -285,7 +284,7 @@
   11.55        cases |> map_index (fn (i, ("", _)) => string_of_int (i + 1) | (_, (name, _)) => name);
   11.56      val elems = cases |> map (fn (_, (vars, _)) =>
   11.57        Element.Constrains (vars |> map_filter (fn (x, SOME T) => SOME (x, T) | _ => NONE)));
   11.58 -    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair ([], [])) props));
   11.59 +    val concl = cases |> map (fn (_, (_, props)) => (("", []), map (rpair []) props));
   11.60  
   11.61      fun mk_stmt stmt ctxt =
   11.62        let
   11.63 @@ -306,14 +305,14 @@
   11.64            in
   11.65              ctxt' |> (snd o ProofContext.add_fixes_i (map (fn x => (x, NONE, NoSyn)) xs));
   11.66              ctxt' |> ProofContext.add_assms_i ProofContext.assume_export
   11.67 -              [((name, [ContextRules.intro_query NONE]), [(asm, ([], []))])]
   11.68 +              [((name, [ContextRules.intro_query NONE]), [(asm, [])])]
   11.69              |>> (fn [(_, [th])] => th)
   11.70            end;
   11.71          val (ths, ctxt') = ctxt
   11.72            |> (snd o ProofContext.add_fixes_i [(AutoBind.thesisN, NONE, NoSyn)])
   11.73            |> fold_map assume_case (cases ~~ stmt)
   11.74            |-> (fn ths => ProofContext.note_thmss_i [((thatN, []), [(ths, [])])] #> #2 #> pair ths);
   11.75 -      in (([(("", atts), [(thesis, ([], []))])], ths), ctxt') end;
   11.76 +      in (([(("", atts), [(thesis, [])])], ths), ctxt') end;
   11.77    in ((elems, concl), mk_stmt) end;
   11.78  
   11.79  end;
    12.1 --- a/src/Pure/Isar/outer_parse.ML	Sun May 07 00:21:13 2006 +0200
    12.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun May 07 00:22:05 2006 +0200
    12.3 @@ -65,7 +65,7 @@
    12.4    val simple_fixes: token list -> (string * string option) list * token list
    12.5    val term: token list -> string * token list
    12.6    val prop: token list -> string * token list
    12.7 -  val propp: token list -> (string * (string list * string list)) * token list
    12.8 +  val propp: token list -> (string * string list) * token list
    12.9    val termp: token list -> (string * string list) * token list
   12.10    val arguments: token list -> Args.T list * token list
   12.11    val attribs: token list -> Attrib.src list * token list
   12.12 @@ -91,7 +91,7 @@
   12.13    val locale_element: token list -> Element.context Locale.element * token list
   12.14    val context_element: token list -> Element.context * token list
   12.15    val statement: token list ->
   12.16 -    ((bstring * Attrib.src list) * (string * (string list * string list)) list) list * token list
   12.17 +    ((bstring * Attrib.src list) * (string * string list) list) list * token list
   12.18    val general_statement: token list ->
   12.19      (Element.context Locale.element list * Element.statement) * OuterLex.token list
   12.20    val statement_keyword: token list -> string * token list
   12.21 @@ -281,11 +281,8 @@
   12.22  
   12.23  val is_terms = Scan.repeat1 ($$$ "is" |-- term);
   12.24  val is_props = Scan.repeat1 ($$$ "is" |-- prop);
   12.25 -val concl_props = $$$ "concl" |-- !!! is_props;
   12.26 -val any_props = concl_props >> pair [] || is_props -- Scan.optional concl_props [];
   12.27  
   12.28 -val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
   12.29 -val propp' = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
   12.30 +val propp = prop -- Scan.optional ($$$ "(" |-- !!! (is_props --| $$$ ")")) [];
   12.31  val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
   12.32  
   12.33  
   12.34 @@ -363,7 +360,7 @@
   12.35      >> Element.Constrains ||
   12.36    $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
   12.37      >> Element.Assumes ||
   12.38 -  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
   12.39 +  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp))
   12.40      >> Element.Defines ||
   12.41    $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
   12.42      >> Element.Notes;
    13.1 --- a/src/Pure/Isar/proof.ML	Sun May 07 00:21:13 2006 +0200
    13.2 +++ b/src/Pure/Isar/proof.ML	Sun May 07 00:22:05 2006 +0200
    13.3 @@ -47,23 +47,15 @@
    13.4    val fix: (string * string option) list -> state -> state
    13.5    val fix_i: (string * typ option) list -> state -> state
    13.6    val assm: ProofContext.export ->
    13.7 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
    13.8 -    state -> state
    13.9 +    ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   13.10    val assm_i: ProofContext.export ->
   13.11 -    ((string * attribute list) * (term * (term list * term list)) list) list
   13.12 -    -> state -> state
   13.13 -  val assume: ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   13.14 -    state -> state
   13.15 -  val assume_i: ((string * attribute list) * (term * (term list * term list)) list) list
   13.16 -    -> state -> state
   13.17 -  val presume: ((string * Attrib.src list) * (string * (string list * string list)) list) list
   13.18 -    -> state -> state
   13.19 -  val presume_i: ((string * attribute list) * (term * (term list * term list)) list) list
   13.20 -    -> state -> state
   13.21 -  val def: ((string * Attrib.src list) * (string * (string * string list))) list ->
   13.22 -    state -> state
   13.23 -  val def_i: ((string * attribute list) * (string * (term * term list))) list ->
   13.24 -    state -> state
   13.25 +    ((string * attribute list) * (term * term list) list) list -> state -> state
   13.26 +  val assume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   13.27 +  val assume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
   13.28 +  val presume: ((string * Attrib.src list) * (string * string list) list) list -> state -> state
   13.29 +  val presume_i: ((string * attribute list) * (term * term list) list) list -> state -> state
   13.30 +  val def: ((string * Attrib.src list) * (string * (string * string list))) list -> state -> state
   13.31 +  val def_i: ((string * attribute list) * (string * (term * term list))) list -> state -> state
   13.32    val chain: state -> state
   13.33    val chain_facts: thm list -> state -> state
   13.34    val get_thmss: state -> (thmref * Attrib.src list) list -> thm list
   13.35 @@ -114,25 +106,19 @@
   13.36    val global_done_proof: state -> context * theory
   13.37    val global_skip_proof: bool -> state -> context * theory
   13.38    val have: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   13.39 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   13.40 -    bool -> state -> state
   13.41 +    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   13.42    val have_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   13.43 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
   13.44 -    bool -> state -> state
   13.45 +    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   13.46    val show: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   13.47 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   13.48 -    bool -> state -> state
   13.49 +    ((string * Attrib.src list) * (string * string list) list) list -> bool -> state -> state
   13.50    val show_i: Method.text option -> (thm list list -> state -> state Seq.seq) ->
   13.51 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
   13.52 -    bool -> state -> state
   13.53 +    ((string * attribute list) * (term * term list) list) list -> bool -> state -> state
   13.54    val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
   13.55      string option -> string * Attrib.src list ->
   13.56 -    ((string * Attrib.src list) * (string * (string list * string list)) list) list ->
   13.57 -    context -> state
   13.58 +    ((string * Attrib.src list) * (string * string list) list) list -> context -> state
   13.59    val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->
   13.60      string option -> string * attribute list ->
   13.61 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
   13.62 -    context -> state
   13.63 +    ((string * attribute list) * (term * term list) list) list -> context -> state
   13.64  end;
   13.65  
   13.66  structure Proof: PROOF =
   13.67 @@ -580,7 +566,7 @@
   13.68    in
   13.69      state'
   13.70      |> fix (map (rpair NONE) xs)
   13.71 -    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, ([], []))]) eqs)
   13.72 +    |> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs)
   13.73    end;
   13.74  
   13.75  in
   13.76 @@ -681,7 +667,7 @@
   13.77      val atts = map (prep_att (theory_of state)) raw_atts;
   13.78      val (asms, state') = state |> map_context_result (fn ctxt =>
   13.79        ctxt |> ProofContext.apply_case (ProofContext.get_case ctxt name xs));
   13.80 -    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
   13.81 +    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair []) ts));
   13.82    in
   13.83      state'
   13.84      |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
    14.1 --- a/src/Pure/Isar/proof_context.ML	Sun May 07 00:21:13 2006 +0200
    14.2 +++ b/src/Pure/Isar/proof_context.ML	Sun May 07 00:22:05 2006 +0200
    14.3 @@ -88,21 +88,21 @@
    14.4    val auto_bind_facts: term list -> context -> context
    14.5    val match_bind: bool -> (string list * string) list -> context -> term list * context
    14.6    val match_bind_i: bool -> (term list * term) list -> context -> term list * context
    14.7 -  val read_propp: context * (string * (string list * string list)) list list
    14.8 -    -> context * (term * (term list * term list)) list list
    14.9 -  val cert_propp: context * (term * (term list * term list)) list list
   14.10 -    -> context * (term * (term list * term list)) list list
   14.11 -  val read_propp_schematic: context * (string * (string list * string list)) list list
   14.12 -    -> context * (term * (term list * term list)) list list
   14.13 -  val cert_propp_schematic: context * (term * (term list * term list)) list list
   14.14 -    -> context * (term * (term list * term list)) list list
   14.15 -  val bind_propp: context * (string * (string list * string list)) list list
   14.16 +  val read_propp: context * (string * string list) list list
   14.17 +    -> context * (term * term list) list list
   14.18 +  val cert_propp: context * (term * term list) list list
   14.19 +    -> context * (term * term list) list list
   14.20 +  val read_propp_schematic: context * (string * string list) list list
   14.21 +    -> context * (term * term list) list list
   14.22 +  val cert_propp_schematic: context * (term * term list) list list
   14.23 +    -> context * (term * term list) list list
   14.24 +  val bind_propp: context * (string * string list) list list
   14.25      -> context * (term list list * (context -> context))
   14.26 -  val bind_propp_i: context * (term * (term list * term list)) list list
   14.27 +  val bind_propp_i: context * (term * term list) list list
   14.28      -> context * (term list list * (context -> context))
   14.29 -  val bind_propp_schematic: context * (string * (string list * string list)) list list
   14.30 +  val bind_propp_schematic: context * (string * string list) list list
   14.31      -> context * (term list list * (context -> context))
   14.32 -  val bind_propp_schematic_i: context * (term * (term list * term list)) list list
   14.33 +  val bind_propp_schematic_i: context * (term * term list) list list
   14.34      -> context * (term list list * (context -> context))
   14.35    val fact_tac: thm list -> int -> tactic
   14.36    val some_fact_tac: context -> int -> tactic
   14.37 @@ -142,10 +142,10 @@
   14.38    val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a)
   14.39    val bind_fixes: string list -> context -> (term -> term) * context
   14.40    val add_assms: export ->
   14.41 -    ((string * attribute list) * (string * (string list * string list)) list) list ->
   14.42 +    ((string * attribute list) * (string * string list) list) list ->
   14.43      context -> (bstring * thm list) list * context
   14.44    val add_assms_i: export ->
   14.45 -    ((string * attribute list) * (term * (term list * term list)) list) list ->
   14.46 +    ((string * attribute list) * (term * term list) list) list ->
   14.47      context -> (bstring * thm list) list * context
   14.48    val assume_export: export
   14.49    val presume_export: export
   14.50 @@ -833,11 +833,12 @@
   14.51  
   14.52  (* simult_matches *)
   14.53  
   14.54 -fun simult_matches ctxt [] = []
   14.55 -  | simult_matches ctxt pairs =
   14.56 +fun simult_matches _ (_, []) = []
   14.57 +  | simult_matches ctxt (t, pats) =
   14.58        let
   14.59          fun fail () = error "Pattern match failed!";
   14.60  
   14.61 +        val pairs = map (rpair t) pats;
   14.62          val maxidx = fold (fn (t1, t2) => fn i =>
   14.63            Int.max (Int.max (Term.maxidx_of_term t1, Term.maxidx_of_term t2), i)) pairs ~1;
   14.64          val envs = Unify.smash_unifiers (theory_of ctxt, Envir.empty maxidx,
   14.65 @@ -885,8 +886,8 @@
   14.66  fun prep_bind prep_pats (raw_pats, t) ctxt =
   14.67    let
   14.68      val ctxt' = declare_term t ctxt;
   14.69 -    val pats = prep_pats (fastype_of t) ctxt' raw_pats;
   14.70 -    val binds = simult_matches ctxt' (map (rpair t) pats);
   14.71 +    val pats = prep_pats (Term.fastype_of t) ctxt' raw_pats;
   14.72 +    val binds = simult_matches ctxt' (t, pats);
   14.73    in (binds, ctxt') end;
   14.74  
   14.75  fun gen_binds prep_terms prep_pats gen raw_binds ctxt =
   14.76 @@ -919,23 +920,18 @@
   14.77  
   14.78  fun prep_propp schematic prep_props prep_pats (context, args) =
   14.79    let
   14.80 -    fun prep (_, (raw_pats1, raw_pats2)) (ctxt, prop :: props) =
   14.81 -          let
   14.82 -            val ctxt' = declare_term prop ctxt;
   14.83 -            val pats = prep_pats ctxt' (raw_pats1 @ raw_pats2);    (*simultaneous type inference!*)
   14.84 -          in ((prop, chop (length raw_pats1) pats), (ctxt', props)) end
   14.85 +    fun prep (_, raw_pats) (ctxt, prop :: props) =
   14.86 +          let val ctxt' = declare_term prop ctxt
   14.87 +          in ((prop, prep_pats ctxt' raw_pats), (ctxt', props)) end
   14.88        | prep _ _ = sys_error "prep_propp";
   14.89      val (propp, (context', _)) = (fold_map o fold_map) prep args
   14.90        (context, prep_props schematic context (maps (map fst) args));
   14.91    in (context', propp) end;
   14.92  
   14.93 -fun matches ctxt (prop, (pats1, pats2)) =
   14.94 -  simult_matches ctxt (map (rpair prop) pats1 @ map (rpair (Logic.strip_imp_concl prop)) pats2);
   14.95 -
   14.96  fun gen_bind_propp prepp (ctxt, raw_args) =
   14.97    let
   14.98      val (ctxt', args) = prepp (ctxt, raw_args);
   14.99 -    val binds = flat (flat (map (map (matches ctxt')) args));
  14.100 +    val binds = flat (flat (map (map (simult_matches ctxt')) args));
  14.101      val propss = map (map #1) args;
  14.102  
  14.103      (*generalize result: context evaluated now, binds added later*)
    15.1 --- a/src/Pure/Isar/specification.ML	Sun May 07 00:21:13 2006 +0200
    15.2 +++ b/src/Pure/Isar/specification.ML	Sun May 07 00:22:05 2006 +0200
    15.3 @@ -46,7 +46,7 @@
    15.4      val (vars, vars_ctxt) = ctxt |> prep_vars raw_vars;
    15.5      val (xs, params_ctxt) = vars_ctxt |> ProofContext.add_fixes_i vars;
    15.6      val ((specs, vs), specs_ctxt) =
    15.7 -      prep_propp (params_ctxt, map (map (rpair ([], [])) o snd) raw_specs)
    15.8 +      prep_propp (params_ctxt, map (map (rpair []) o snd) raw_specs)
    15.9        |> swap |>> map (map fst)
   15.10        ||>> fold_map ProofContext.inferred_param xs;
   15.11  
    16.1 --- a/src/Pure/Tools/class_package.ML	Sun May 07 00:21:13 2006 +0200
    16.2 +++ b/src/Pure/Tools/class_package.ML	Sun May 07 00:22:05 2006 +0200
    16.3 @@ -301,7 +301,7 @@
    16.4    thy
    16.5    |> ProofContext.init
    16.6    |> Proof.theorem_i PureThy.internalK NONE (after_qed oo (fold o fold) add_thm) NONE ("", [])
    16.7 -       (map (fn t => (("", []), [(t, ([], []))])) (mk_prop thy inst));
    16.8 +       (map (fn t => (("", []), [(t, [])])) (mk_prop thy inst));
    16.9  
   16.10  in
   16.11  
    17.1 --- a/src/Pure/axclass.ML	Sun May 07 00:21:13 2006 +0200
    17.2 +++ b/src/Pure/axclass.ML	Sun May 07 00:22:05 2006 +0200
    17.3 @@ -283,7 +283,7 @@
    17.4        |> map_term_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    17.5        |> Logic.close_form;
    17.6  
    17.7 -    val axiomss = prep_propp (ctxt, map (map (rpair ([], [])) o snd) raw_specs)
    17.8 +    val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    17.9        |> snd |> map (map (prep_axiom o fst));
   17.10      val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
   17.11