--- 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 *)