# HG changeset patch
# User wenzelm
# Date 1011297983 -3600
# Node ID a529b4b918883eac4baf99e073fe70cf38ec3b3a
# Parent  4f2983e39a59c33117b4daf3cf7af37fc820dec8
RuleCases.make interface based on term instead of thm;
tuned;

diff -r 4f2983e39a59 -r a529b4b91888 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jan 17 21:05:58 2002 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Jan 17 21:06:23 2002 +0100
@@ -479,11 +479,10 @@
     val th = raw_th RS Drule.rev_triv_goal;
     val ths = Drule.conj_elim_precise (length ts) th
       handle THM _ => err "Main goal structure corrupted";
-    val props = map (#prop o Thm.rep_thm) ths;
   in
     conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
         cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
-    conditional (exists (not o Pattern.matches tsig) (ts ~~ props)) (fn () =>
+    conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () =>
       err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th)));
     ths
   end;
@@ -641,9 +640,10 @@
       |> enter_forward
       |> opt_block
       |> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
+    val sign' = sign_of state';
 
     val props = flat propss;
-    val cprop = Thm.cterm_of (sign_of state') (Logic.mk_conjunction_list props);
+    val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
     val goal = Drule.mk_triv_goal cprop;
 
     val tvars = foldr Term.add_term_tvars (props, []);
@@ -659,7 +659,8 @@
     |> map_context (autofix props)
     |> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds))
     |> map_context (ProofContext.add_cases
-     (if length props = 1 then RuleCases.make true goal [rule_contextN]
+     (if length props = 1 then
+      RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
       else [(rule_contextN, RuleCases.empty)]))
     |> auto_bind_goal props
     |> (if is_chain state then use_facts else reset_facts)