1.1 --- a/src/Pure/Isar/proof.ML	Sat Jan 07 12:26:31 2006 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Sat Jan 07 12:26:32 2006 +0100
     1.3 @@ -390,7 +390,7 @@
     1.4  fun no_goal_cases st = map (rpair NONE) (goals st);
     1.5  
     1.6  fun goal_cases st =
     1.7 -  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
     1.8 +  RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
     1.9  
    1.10  fun check_theory thy state =
    1.11    if subthy (thy, theory_of state) then state
    1.12 @@ -663,13 +663,11 @@
    1.13  fun gen_invoke_case prep_att (name, xs, raw_atts) state =
    1.14    let
    1.15      val atts = map (prep_att (theory_of state)) raw_atts;
    1.16 -    val ((lets, asms), state') =
    1.17 +    val (asms, state') =
    1.18        map_context_result (ProofContext.apply_case (get_case state name xs)) state;
    1.19 -    val assumptions = asms |> map (fn (a, ts) =>
    1.20 -      ((NameSpace.qualified name a, atts), map (rpair ([], [])) ts));
    1.21 +    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
    1.22    in
    1.23      state'
    1.24 -    |> add_binds_i lets
    1.25      |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
    1.26      |> assume_i assumptions
    1.27      |> add_binds_i AutoBind.no_facts