# HG changeset patch
# User wenzelm
# Date 1427657428 -7200
# Node ID c648efffea739ff0da180fdee1db82f06d9c7224
# Parent  b640b5e6b023893daccf3695193b51462f31dd88
support for minimal specifications, with usual treatment of fixes and dummies;

diff -r b640b5e6b023 -r c648efffea73 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Mar 29 20:40:49 2015 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Mar 29 21:30:28 2015 +0200
@@ -7,6 +7,10 @@
 
 signature SPECIFICATION =
 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:
     (binding * typ option * mixfix) list -> (Attrib.binding * term) list -> Proof.context ->
     (((binding * typ) * mixfix) list * (Attrib.binding * term) list) * Proof.context
@@ -79,6 +83,22 @@
 structure Specification: SPECIFICATION =
 struct
 
+(* prepare propositions *)
+
+fun read_props raw_props raw_fixes ctxt =
+  let
+    val ctxt1 = ctxt |> Proof_Context.read_vars raw_fixes |-> Proof_Context.add_fixes |> #2;
+    val props1 = map (Syntax.parse_prop ctxt1) raw_props;
+    val (props2, ctxt2) = ctxt1 |> fold_map Variable.fix_dummy_patterns props1;
+    val props3 = Syntax.check_props ctxt2 props2;
+    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 *)
 
 local