# HG changeset patch
# User wenzelm
# Date 937927475 -7200
# Node ID f3e78ebcf6baab06681e64588cf2986599fa071b
# Parent  dd281afb33d751c440803cb3179934f91416d7ee
setup_goal: do not insert assumptions;

diff -r dd281afb33d7 -r f3e78ebcf6ba src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Sep 21 17:23:55 1999 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Sep 21 17:24:35 1999 +0200
@@ -585,11 +585,15 @@
       |> enter_forward
       |> map_context_result (fn c => prepp (c, raw_propp));
     val cprop = Thm.cterm_of (sign_of state') prop;
+(* FIXME
     val casms = map #1 (assumptions state');
 
     val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
     fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
+
     val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
+*)
+    val goal = Drule.mk_triv_goal cprop;
   in
     state'
     |> opt_block