# HG changeset patch
# User wenzelm
# Date 1395137618 -3600
# Node ID 1f9951be72b5e0ef84357928193f15f1f53b688b
# Parent  8e8d28ed752957d53efbc2e836b7063786b269e9
unused;

diff -r 8e8d28ed7529 -r 1f9951be72b5 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Tue Mar 18 11:07:47 2014 +0100
+++ b/src/Pure/Isar/args.ML	Tue Mar 18 11:13:38 2014 +0100
@@ -65,8 +65,6 @@
   val parse1: (string -> bool) -> Token.T list parser
   val attribs: (xstring * Position.T -> string) -> src list parser
   val opt_attribs: (xstring * Position.T -> string) -> src list parser
-  val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
-  val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
   val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
 end;
@@ -304,16 +302,6 @@
 fun opt_attribs check = Scan.optional (attribs check) [];
 
 
-(* theorem specifications *)
-
-fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
-
-fun opt_thm_name check_attrib s =
-  Scan.optional
-    ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
-    (Binding.empty, []);
-
-
 
 (** syntax wrapper **)