setup_goal: do not insert assumptions;
authorwenzelm
Tue Sep 21 17:24:35 1999 +0200 (1999-09-21)
changeset 7556f3e78ebcf6ba
parent 7555 dd281afb33d7
child 7557 1b977741f530
setup_goal: do not insert assumptions;
src/Pure/Isar/proof.ML
     1.1 --- a/src/Pure/Isar/proof.ML	Tue Sep 21 17:23:55 1999 +0200
     1.2 +++ b/src/Pure/Isar/proof.ML	Tue Sep 21 17:24:35 1999 +0200
     1.3 @@ -585,11 +585,15 @@
     1.4        |> enter_forward
     1.5        |> map_context_result (fn c => prepp (c, raw_propp));
     1.6      val cprop = Thm.cterm_of (sign_of state') prop;
     1.7 +(* FIXME
     1.8      val casms = map #1 (assumptions state');
     1.9  
    1.10      val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl;
    1.11      fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm);
    1.12 +
    1.13      val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop);
    1.14 +*)
    1.15 +    val goal = Drule.mk_triv_goal cprop;
    1.16    in
    1.17      state'
    1.18      |> opt_block