unused;
authorwenzelm
Tue Mar 18 11:13:38 2014 +0100 (2014-03-18)
changeset 562001f9951be72b5
parent 56199 8e8d28ed7529
child 56201 dd2df97b379b
unused;
src/Pure/Isar/args.ML
     1.1 --- a/src/Pure/Isar/args.ML	Tue Mar 18 11:07:47 2014 +0100
     1.2 +++ b/src/Pure/Isar/args.ML	Tue Mar 18 11:13:38 2014 +0100
     1.3 @@ -65,8 +65,6 @@
     1.4    val parse1: (string -> bool) -> Token.T list parser
     1.5    val attribs: (xstring * Position.T -> string) -> src list parser
     1.6    val opt_attribs: (xstring * Position.T -> string) -> src list parser
     1.7 -  val thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
     1.8 -  val opt_thm_name: (xstring * Position.T -> string) -> string -> (binding * src list) parser
     1.9    val syntax_generic: 'a context_parser -> src -> Context.generic -> 'a * Context.generic
    1.10    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
    1.11  end;
    1.12 @@ -304,16 +302,6 @@
    1.13  fun opt_attribs check = Scan.optional (attribs check) [];
    1.14  
    1.15  
    1.16 -(* theorem specifications *)
    1.17 -
    1.18 -fun thm_name check_attrib s = binding -- opt_attribs check_attrib --| $$$ s;
    1.19 -
    1.20 -fun opt_thm_name check_attrib s =
    1.21 -  Scan.optional
    1.22 -    ((binding -- opt_attribs check_attrib || attribs check_attrib >> pair Binding.empty) --| $$$ s)
    1.23 -    (Binding.empty, []);
    1.24 -
    1.25 -
    1.26  
    1.27  (** syntax wrapper **)
    1.28