# HG changeset patch
# User wenzelm
# Date 1153935462 -7200
# Node ID 3bff4719f3d65e52039699a93f56d8803c5f6f0a
# Parent  be3bfb0699ba247abcbbfa8e73375bd0e8d2538b
focus: result record includes (fixed) schematic variables;
SUBGOAL: disallow pending subgoals, more robust re-composition;

diff -r be3bfb0699ba -r 3bff4719f3d6 src/Pure/subgoal.ML
--- a/src/Pure/subgoal.ML	Wed Jul 26 19:37:41 2006 +0200
+++ b/src/Pure/subgoal.ML	Wed Jul 26 19:37:42 2006 +0200
@@ -8,16 +8,17 @@
 signature BASIC_SUBGOAL =
 sig
   val SUBPROOF: Proof.context ->
-    ({context: Proof.context, asms: cterm list, concl: cterm,
-      params: (string * typ) list, prems: thm list} -> tactic) -> int -> tactic
+    ({context: Proof.context, schematics: ctyp list * cterm list,
+      params: cterm list, asms: cterm list, concl: cterm,
+      prems: thm list} -> tactic) -> int -> tactic
 end
 
 signature SUBGOAL =
 sig
   include BASIC_SUBGOAL
   val focus: Proof.context -> int -> thm ->
-   {context: Proof.context, asms: cterm list, concl: cterm,
-    params: (string * typ) list, prems: thm list} * thm
+   {context: Proof.context, schematics: ctyp list * cterm list,
+    params: cterm list, asms: cterm list, concl: cterm, prems: thm list} * thm
 
 end;
 
@@ -28,23 +29,28 @@
 
 fun focus ctxt i st =
   let
-    val ([st'], ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
+    val ((schematics, [st']), ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
     val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
     val asms = Drule.strip_imp_prems goal;
     val concl = Drule.strip_imp_concl goal;
     val (prems, context) = ProofContext.add_assumes asms ctxt'';
   in
-    ({context = context, asms = asms, concl = concl, params = params, prems = prems},
-      Goal.init concl)
+    ({context = context, schematics = schematics, params = params,
+      asms = asms, concl = concl, prems = prems}, Goal.init concl)
   end;
 
 fun SUBPROOF ctxt tac i st =
   if Thm.nprems_of st < i then Seq.empty
   else
     let
-      val (args as {context, ...}, st') = focus ctxt i st
-      val result = Goal.conclude #> Seq.singleton (ProofContext.goal_exports context ctxt);
-    in Seq.lifts (fn res => Proof.goal_tac res i) (Seq.maps result (tac args st')) st end
+      val (args as {context, params, ...}, st') = focus ctxt i st;
+      fun export_closed th =
+        let
+          val (th' :: params') = ProofContext.export context ctxt (th :: map Drule.mk_term params);
+          val vs = map (#2 o Thm.dest_comb o Drule.strip_imp_concl o Thm.cprop_of) params';
+        in Drule.forall_intr_list vs th' end;
+      fun retrofit th = Thm.compose_no_flatten false (th, 0) i;
+    in Seq.lifts retrofit (Seq.map (Goal.finish #> export_closed) (tac args st')) st end
 
 end;