changeset 11924 | b6def266cbb9 |
parent 11917 | 9a0a736d820b |
child 11985 | 06658189cd51 |
--- a/src/Pure/Isar/proof.ML Wed Oct 24 17:38:29 2001 +0200 +++ b/src/Pure/Isar/proof.ML Wed Oct 24 19:18:10 2001 +0200 @@ -515,9 +515,7 @@ state |> assert_forward |> map_context_result (f exp args) - |> (fn (st, (factss, prems)) => - these_factss (st, factss) - |> put_thms ("prems", prems)); + |> these_factss; val assm = gen_assume ProofContext.assume; val assm_i = gen_assume ProofContext.assume_i;