# HG changeset patch
# User wenzelm
# Date 931538715 -7200
# Node ID a0b34115077f227c5c940798276131747ab5ca5e
# Parent  01f3c7866ead265aec44877321e3ad3d8e411a5d
added termp;

diff -r 01f3c7866ead -r a0b34115077f src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Jul 09 18:44:58 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Jul 09 18:45:15 1999 +0200
@@ -50,6 +50,7 @@
   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 termp: token list -> (string * string list) * token list
   val attribs: token list -> Args.src list * token list
   val opt_attribs: token list -> Args.src list * token list
   val thm_name: string -> token list -> (bstring * Args.src list) * token list
@@ -224,13 +225,15 @@
 val prop = group "proposition" trm;
 
 
-(* prop patters *)
+(* patterns *)
 
+val is_terms = Scan.repeat1 ($$$ "is" |-- term);
 val is_props = Scan.repeat1 ($$$ "is" |-- prop);
 val concl_props = $$$ "concl" |-- !!! is_props;
 val any_props = is_props -- Scan.optional concl_props [] || concl_props >> pair [];
 
 val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
+val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
 
 
 (* arguments *)