# HG changeset patch
# User wenzelm
# Date 947068813 -3600
# Node ID 8efec140c5e4f1a2d021d85a10a09498565a2e7a
# Parent  6ae943d080de66049f33409ec762704344d8615a
removed pats;

diff -r 6ae943d080de -r 8efec140c5e4 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Jan 05 11:38:48 2000 +0100
+++ b/src/Pure/Isar/args.ML	Wed Jan 05 11:40:13 2000 +0100
@@ -29,13 +29,9 @@
   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_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_term_pat: Proof.context * T list -> term * (Proof.context * T list)
-  val local_prop_pat: Proof.context * T list -> term * (Proof.context * T list)
   val bang_facts: Proof.context * T list -> thm list * (Proof.context * T list)
   type src
   val src: (string * T list) * Position.T -> src
@@ -131,14 +127,10 @@
 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_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_term_pat = gen_item ProofContext.read_term_pat;
-val local_prop_pat = gen_item ProofContext.read_prop_pat;
 
 
 (* bang facts *)