changeset 30757 | 2d2076300185 |
parent 30585 | 6b2ba4666336 |
child 30763 | 6976521b4263 |
--- a/src/Pure/Isar/obtain.ML Sat Mar 28 16:30:09 2009 +0100 +++ b/src/Pure/Isar/obtain.ML Sat Mar 28 16:31:16 2009 +0100 @@ -294,7 +294,7 @@ |> Proof.fix_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) parms) |> `Proof.context_of |-> (fn fix_ctxt => Proof.assm_i (obtain_export fix_ctxt rule (map cert ts)) [(Thm.empty_binding, asms)]) - |> Proof.add_binds_i AutoBind.no_facts + |> Proof.bind_terms AutoBind.no_facts end; val goal = Var (("guess", 0), propT);