# HG changeset patch
# User wenzelm
# Date 1464601481 -7200
# Node ID ee1c9de4e03ac45addd7eb765c907b14a2ed35d4
# Parent  ddfd021884b49443b6b05c9cd4aa5f360be046c5
unused;

diff -r ddfd021884b4 -r ee1c9de4e03a src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun May 29 15:40:25 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Mon May 30 11:44:41 2016 +0200
@@ -9,8 +9,6 @@
 sig
   val read_props: string list -> (binding * string option * mixfix) list -> Proof.context ->
     term list * Proof.context
-  val read_prop: string -> (binding * string option * mixfix) list -> Proof.context ->
-    term * Proof.context
   val check_spec_open: (binding * typ option * mixfix) list ->
     (binding * typ option * mixfix) list -> term list -> term -> Proof.context ->
     ((binding * typ option * mixfix) list * string list * (string -> Position.T) * term) *
@@ -90,10 +88,6 @@
     val ctxt3 = ctxt2 |> fold Variable.declare_term props3;
   in (props3, ctxt3) end;
 
-fun read_prop raw_prop raw_fixes ctxt =
-  let val ([prop], ctxt') = read_props [raw_prop] raw_fixes ctxt
-  in (prop, ctxt') end;
-
 
 (* prepare specification *)