# HG changeset patch
# User wenzelm
# Date 931451769 -7200
# Node ID a3f3f4128cab4b267043d3b7dd9ba5a0b915074d
# Parent  04d051190a5f53820d9c9d865196e80cb7201f4a
propp: 'concl' patterns;

diff -r 04d051190a5f -r a3f3f4128cab src/HOL/Tools/typedef_package.ML
--- a/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:35:44 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:36:09 1999 +0200
@@ -195,7 +195,7 @@
     val goal = Thm.term_of (goal_nonempty cset);
   in
     thy
-    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
+    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;
diff -r 04d051190a5f -r a3f3f4128cab src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Thu Jul 08 18:36:09 1999 +0200
@@ -49,6 +49,7 @@
   val const: token list -> (bstring * string * Syntax.mixfix) * token list
   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 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
@@ -223,6 +224,15 @@
 val prop = group "proposition" trm;
 
 
+(* prop patters *)
+
+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 --| $$$ ")")) ([], []);
+
+
 (* arguments *)
 
 val keyword_symid = Scan.one (OuterLex.keyword_pred OuterLex.is_sid) >> OuterLex.val_of;
diff -r 04d051190a5f -r a3f3f4128cab src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Thu Jul 08 18:36:09 1999 +0200
@@ -38,8 +38,8 @@
     val thm = Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof);
   in Method.METHOD (fn _ => ALLGOALS (Tactic.rtac thm)) end;
 
-val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth);
-val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth);
+val local_skip_proof = Method.local_terminal_proof (Method.Basic cheat_meth, None);
+val global_skip_proof = Method.global_terminal_proof (Method.Basic cheat_meth, None);
 
 
 (* proof command *)
diff -r 04d051190a5f -r a3f3f4128cab src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Jul 08 18:35:44 1999 +0200
+++ b/src/Pure/axclass.ML	Thu Jul 08 18:36:09 1999 +0200
@@ -408,7 +408,7 @@
 fun inst_proof mk_prop add_thms (sig_prop, comment) int thy =
   thy
   |> IsarThy.theorem_i (("", [inst_attribute add_thms],
-    (mk_prop (Theory.sign_of thy) sig_prop, [])), comment) int;
+    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))), comment) int;
 
 val instance_subclass_proof = inst_proof (mk_classrel oo intrn_classrel) add_classrel_thms;
 val instance_subclass_proof_i = inst_proof (K mk_classrel) add_classrel_thms;