changeset 6996 | 1a28d968c5aa |
parent 6985 | 2af6405a6ef3 |
child 7200 | c9b03d9d6647 |
--- a/src/Pure/Isar/proof_context.ML Tue Jul 13 13:53:34 1999 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Jul 13 13:54:08 1999 +0200 @@ -660,7 +660,7 @@ val cprops = map (Thm.cterm_of sign) props; val cprops_tac = map (rpair tac) cprops; - val asms = map (Drule.forall_elim_vars (maxidx + 1) o Thm.assume) cprops; + val asms = map (Drule.forall_elim_vars (maxidx + 1) o Drule.assume_goal) cprops; val ths = map (fn th => ([th], [])) asms; val (ctxt'', (_, thms)) =