--- a/src/Pure/Isar/proof.ML Tue Oct 09 19:24:19 2012 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 09 20:05:17 2012 +0200
@@ -643,7 +643,11 @@
|>> map (fn (x, _, mx) => (x, mx))
|-> (fn vars =>
map_context_result (prep_binds false (map swap raw_rhss))
- #-> (fn rhss => map_context_result (Local_Defs.add_defs (vars ~~ (name_atts ~~ rhss)))))
+ #-> (fn rhss =>
+ let
+ val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
+ ((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
+ in map_context_result (Local_Defs.add_defs defs) end))
|-> (set_facts o map (#2 o #2))
end;