--- a/src/Pure/Isar/generic_target.ML Wed Mar 14 11:10:10 2012 +0100
+++ b/src/Pure/Isar/generic_target.ML Wed Mar 14 11:45:16 2012 +0100
@@ -48,13 +48,11 @@
(* define *)
-fun define foundation ((b, mx), ((proto_b_def, atts), rhs)) lthy =
+fun define foundation ((b, mx), ((b_def, atts), rhs)) lthy =
let
val thy = Proof_Context.theory_of lthy;
val thy_ctxt = Proof_Context.init_global thy;
- val b_def = Thm.def_binding_optional b proto_b_def;
-
(*term and type parameters*)
val crhs = Thm.cterm_of thy rhs;
val ((defs, _), rhs') = Local_Defs.export_cterm lthy thy_ctxt crhs ||> Thm.term_of;
@@ -202,7 +200,8 @@
val lhs = list_comb (const, type_params @ term_params);
val ((_, def), lthy3) = lthy2
|> Local_Theory.background_theory_result
- (Thm.add_def lthy2 false false (b_def, Logic.mk_equals (lhs, rhs)));
+ (Thm.add_def lthy2 false false
+ (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs)));
in ((lhs, def), lthy3) end;
fun theory_notes kind global_facts lthy =