1.1 --- a/src/Pure/subgoal.ML	Thu Jul 27 13:43:08 2006 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Thu Jul 27 13:43:09 2006 +0200
     1.3 @@ -7,10 +7,10 @@
     1.4  
     1.5  signature BASIC_SUBGOAL =
     1.6  sig
     1.7 -  val SUBPROOF: Proof.context ->
     1.8 +  val SUBPROOF:
     1.9      ({context: Proof.context, schematics: ctyp list * cterm list,
    1.10        params: cterm list, asms: cterm list, concl: cterm,
    1.11 -      prems: thm list} -> tactic) -> int -> tactic
    1.12 +      prems: thm list} -> tactic) -> Proof.context -> int -> tactic
    1.13  end
    1.14  
    1.15  signature SUBGOAL =
    1.16 @@ -29,17 +29,17 @@
    1.17  
    1.18  fun focus ctxt i st =
    1.19    let
    1.20 -    val ((schematics, [st']), ctxt') = Variable.import true [Goal.norm_hhf st] ctxt;
    1.21 +    val ((schematics, [st']), ctxt') = Variable.import true [norm_hhf st] ctxt;
    1.22      val ((params, goal), ctxt'') = Variable.focus (Thm.cprem_of st' i) ctxt';
    1.23      val asms = Drule.strip_imp_prems goal;
    1.24      val concl = Drule.strip_imp_concl goal;
    1.25 -    val (prems, context) = ProofContext.add_assumes asms ctxt'';
    1.26 +    val (prems, context) = Assumption.add_assumes asms ctxt'';
    1.27    in
    1.28      ({context = context, schematics = schematics, params = params,
    1.29        asms = asms, concl = concl, prems = prems}, Goal.init concl)
    1.30    end;
    1.31  
    1.32 -fun SUBPROOF ctxt tac i st =
    1.33 +fun SUBPROOF tac ctxt i st =
    1.34    if Thm.nprems_of st < i then Seq.empty
    1.35    else
    1.36      let