--- a/src/Pure/Isar/proof_context.ML Sun Oct 14 20:09:05 2001 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Oct 14 20:09:19 2001 +0200
@@ -693,8 +693,11 @@
val add_binds = gen_binds read_term;
val add_binds_i = gen_binds cert_term;
-val auto_bind_goal = add_binds_i o map drop_schematic o AutoBind.goal;
-val auto_bind_facts = (add_binds_i o map drop_schematic) oo AutoBind.facts;
+fun auto_bind_goal t ctxt =
+ ctxt |> add_binds_i (map drop_schematic (AutoBind.goal (sign_of ctxt) t));
+
+fun auto_bind_facts name ts ctxt =
+ ctxt |> add_binds_i (map drop_schematic (AutoBind.facts (sign_of ctxt) name ts));
end;