src/Pure/Isar/proof.ML

   val fix_i: (string list * typ option) list -> state -> state
   val norm_hhf_tac: int -> tactic
   val hard_asm_tac: int -> tactic
   val soft_asm_tac: int -> tactic
   val assm: ProofContext.exporter
-    -> (string * context attribute list * (string * (string list * string list)) list) list
+    -> ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
   val assm_i: ProofContext.exporter
-    -> (string * context attribute list * (term * (term list * term list)) list) list
+    -> ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val assume: (string * context attribute list * (string * (string list * string list)) list) list
+  val assume:
+    ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
-  val assume_i: (string * context attribute list * (term * (term list * term list)) list) list
+  val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
-  val presume: (string * context attribute list * (string * (string list * string list)) list) list
+  val presume:
+    ((string * context attribute list) * (string * (string list * string list)) list) list
     -> state -> state
-  val presume_i: (string * context attribute list * (term * (term list * term list)) list) list
+  val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
     -> state -> state
   val invoke_case: string * context attribute list -> state -> state
   val theorem: bstring -> theory attribute list -> string * (string list * string list)
     -> theory -> state
   val theorem_i: bstring -> theory attribute list -> term * (term list * term list)

     val (vars, props) = get_case state name;
     val bind_skolem = ProofContext.bind_skolem (context_of state) (map #1 vars);
   in
     state
     |> fix_i (map (fn (x, T) => ([x], Some T)) vars)
-    |> assume_i [(name, atts, map (fn t => (t, ([], []))) (map bind_skolem props))]
+    |> assume_i [((name, atts), map (fn t => (t, ([], []))) (map bind_skolem props))]
   end;
 
 
 
 (** goals **)

 
 val antN = "antecedent";
 
 fun setup_goal opt_block prepp kind after_qed name atts raw_propp state =
   let
-    val (state', (prop, gen_binds)) =
+    val (state', ([[prop]], gen_binds)) =
       state
       |> assert_forward_or_chain
       |> enter_forward
       |> opt_block
-      |> map_context_result (fn ct => prepp (ct, raw_propp));
+      |> map_context_result (fn ct => prepp (ct, [[raw_propp]]));
     val cprop = Thm.cterm_of (sign_of state') prop;
     val goal = Drule.mk_triv_goal cprop;
   in
     state'
     |> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds))