term_pat vs. prop_pat;
authorwenzelm
Thu Nov 19 11:45:26 1998 +0100 (1998-11-19)
changeset 5934ecc224b81f7f
parent 5933 7b0f502a25b1
child 5935 6a82c8a1808f
term_pat vs. prop_pat;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Thu Nov 19 11:44:59 1998 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Thu Nov 19 11:45:26 1998 +0100
     1.3 @@ -29,11 +29,13 @@
     1.4    val global_typ: theory * T list -> typ * (theory * T list)
     1.5    val global_term: theory * T list -> term * (theory * T list)
     1.6    val global_prop: theory * T list -> term * (theory * T list)
     1.7 -  val global_pat: theory * T list -> term * (theory * T list)
     1.8 +  val global_term_pat: theory * T list -> term * (theory * T list)
     1.9 +  val global_prop_pat: theory * T list -> term * (theory * T list)
    1.10    val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
    1.11    val local_term: Proof.context * T list -> term * (Proof.context * T list)
    1.12    val local_prop: Proof.context * T list -> term * (Proof.context * T list)
    1.13 -  val local_pat: Proof.context * T list -> term * (Proof.context * T list)
    1.14 +  val local_term_pat: Proof.context * T list -> term * (Proof.context * T list)
    1.15 +  val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
    1.16    type src
    1.17    val src: (string * T list) * Position.T -> src
    1.18    val dest_src: src -> (string * T list) * Position.T
    1.19 @@ -128,12 +130,14 @@
    1.20  val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
    1.21  val global_term = gen_item (ProofContext.read_term o ProofContext.init);
    1.22  val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
    1.23 -val global_pat = gen_item (ProofContext.read_pat o ProofContext.init);
    1.24 +val global_term_pat = gen_item (ProofContext.read_term_pat o ProofContext.init);
    1.25 +val global_prop_pat = gen_item (ProofContext.read_prop_pat o ProofContext.init);
    1.26  
    1.27  val local_typ = gen_item ProofContext.read_typ;
    1.28  val local_term = gen_item ProofContext.read_term;
    1.29  val local_prop = gen_item ProofContext.read_prop;
    1.30 -val local_pat = gen_item ProofContext.read_pat;
    1.31 +val local_term_pat = gen_item ProofContext.read_term_pat;
    1.32 +val local_prop_pat = gen_item ProofContext.read_prop_pat;
    1.33  
    1.34  
    1.35  (* args *)