src/Tools/interpretation_with_defs.ML
changeset 46909 3c73a121a387
parent 46858 05f30c796f95
child 46947 b8c7eb0c2f89
--- a/src/Tools/interpretation_with_defs.ML	Tue Mar 13 17:17:52 2012 +0000
+++ b/src/Tools/interpretation_with_defs.ML	Tue Mar 13 20:04:24 2012 +0100
@@ -45,8 +45,8 @@
 
     val rhss = map (parse_term defs_ctxt o snd o snd) raw_defs
       |> Syntax.check_terms defs_ctxt;
-    val defs = map2 (fn (binding_thm, (binding_syn, _)) => fn rhs =>
-      (binding_syn, (binding_thm, rhs))) raw_defs rhss;
+    val defs = map2 (fn ((name, atts), ((b, mx), _)) => fn rhs =>
+      ((b, mx), ((Thm.def_binding_optional b name, atts), rhs))) raw_defs rhss;
 
     val (def_eqns, theory') = theory
       |> Named_Target.theory_init