# HG changeset patch
# User wenzelm
# Date 911472326 -3600
# Node ID ecc224b81f7fac71e7284a3161036cbbb29ff7b6
# Parent  7b0f502a25b12b491f08f24070f3c68eccf45c9d
term_pat vs. prop_pat;

diff -r 7b0f502a25b1 -r ecc224b81f7f src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Thu Nov 19 11:44:59 1998 +0100
+++ b/src/Pure/Isar/args.ML	Thu Nov 19 11:45:26 1998 +0100
@@ -29,11 +29,13 @@
   val global_typ: theory * T list -> typ * (theory * T list)
   val global_term: theory * T list -> term * (theory * T list)
   val global_prop: theory * T list -> term * (theory * T list)
-  val global_pat: theory * T list -> term * (theory * T list)
+  val global_term_pat: theory * T list -> term * (theory * T list)
+  val global_prop_pat: theory * T list -> term * (theory * T list)
   val local_typ: Proof.context * T list -> typ * (Proof.context * T list)
   val local_term: Proof.context * T list -> term * (Proof.context * T list)
   val local_prop: Proof.context * T list -> term * (Proof.context * T list)
-  val local_pat: Proof.context * T list -> term * (Proof.context * T list)
+  val local_term_pat: Proof.context * T list -> term * (Proof.context * T list)
+  val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
   type src
   val src: (string * T list) * Position.T -> src
   val dest_src: src -> (string * T list) * Position.T
@@ -128,12 +130,14 @@
 val global_typ = gen_item (ProofContext.read_typ o ProofContext.init);
 val global_term = gen_item (ProofContext.read_term o ProofContext.init);
 val global_prop = gen_item (ProofContext.read_prop o ProofContext.init);
-val global_pat = gen_item (ProofContext.read_pat o ProofContext.init);
+val global_term_pat = gen_item (ProofContext.read_term_pat o ProofContext.init);
+val global_prop_pat = gen_item (ProofContext.read_prop_pat o ProofContext.init);
 
 val local_typ = gen_item ProofContext.read_typ;
 val local_term = gen_item ProofContext.read_term;
 val local_prop = gen_item ProofContext.read_prop;
-val local_pat = gen_item ProofContext.read_pat;
+val local_term_pat = gen_item ProofContext.read_term_pat;
+val local_prop_pat = gen_item ProofContext.read_prop_pat;
 
 
 (* args *)