# HG changeset patch
# User wenzelm
# Date 1136633192 -3600
# Node ID 7b074c340aac0ba663ecdec23a2936f84e87a10c
# Parent  46e7fc90fde3ab03dec7286ce7ca19fe421ae10e
RuleCases.make_common;

diff -r 46e7fc90fde3 -r 7b074c340aac src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Jan 07 12:26:31 2006 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Jan 07 12:26:32 2006 +0100
@@ -390,7 +390,7 @@
 fun no_goal_cases st = map (rpair NONE) (goals st);
 
 fun goal_cases st =
-  RuleCases.make true NONE (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
+  RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st));
 
 fun check_theory thy state =
   if subthy (thy, theory_of state) then state
@@ -663,13 +663,11 @@
 fun gen_invoke_case prep_att (name, xs, raw_atts) state =
   let
     val atts = map (prep_att (theory_of state)) raw_atts;
-    val ((lets, asms), state') =
+    val (asms, state') =
       map_context_result (ProofContext.apply_case (get_case state name xs)) state;
-    val assumptions = asms |> map (fn (a, ts) =>
-      ((NameSpace.qualified name a, atts), map (rpair ([], [])) ts));
+    val assumptions = asms |> map (fn (a, ts) => ((a, atts), map (rpair ([], [])) ts));
   in
     state'
-    |> add_binds_i lets
     |> map_context (ProofContext.qualified_names #> ProofContext.no_base_names)
     |> assume_i assumptions
     |> add_binds_i AutoBind.no_facts