Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
unused;
authorwenzelm
Mon, 30 May 2016 11:44:41 +0200
changeset 63181 ee1c9de4e03a
parent 63180 ddfd021884b4
child 63182 b065b4833092
unused;
src/Pure/Isar/specification.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle